A nondegenerate dyadic simplex determines a unique sphere

Let $A$ have row $i$ equal to $p_i-p_0$ for $i=1,\dots ,d$. Subtracting the first row from every later row of the matrix defining $O_d$ preserves its determinant: multilinearity in each row follows from the finite Leibniz sum, and every added determinant has two equal rows, whose permutation terms cancel in pairs. Expanding along the final column gives $O_d=(-1{)}^d\det A$, so $\det A\mathrm{\ne }0$.

Put $b_i=({\sum }_j{p}_{i,j}^2-{\sum }_j{p}_{0,j}^2)\mathrm{/}2$ for $i=1,\dots ,d$. Since $1>0$ and the order is compatible with addition, $2=1+1>0$ and is nonzero. By [F3] and [step 1.1], there is a unique $c\in {\mathbb{R}}^d$ with $Ac=b$.

Expanding $Ac=b$ gives $2{\sum }_j{c}_j(p_{i,j}-p_{0,j})={\sum }_j{p}_{i,j}^2-{\sum }_j{p}_{0,j}^2$. Rearranging shows ${\sum }_j(p_{i,j}-c_j{)}^2={\sum }_j(p_{0,j}-c_j{)}^2$ for every $i=1,\dots ,d$. Let $s={\sum }_j(p_{0,j}-c_j{)}^2\ge 0$; by [F4], the unique $r\ge 0$ with $r^2=s$ exists. Hence $S(c,r)$ passes through all base points.

If $(c^{\mathrm{\prime }},r^{\mathrm{\prime }})$ is any other center and nonnegative radius through the base points, equal squared distances give $A{c}^{\mathrm{\prime }}=b$. Uniqueness in [F3] forces $c^{\mathrm{\prime }}=c$. Then $r^{\mathrm{\prime }2}=s=r^2$, and uniqueness of the nonnegative square root [F4] gives $r^{\mathrm{\prime }}=r$. All objects are obtained from finite data and unique solutions; no choice axiom is used.