Proof of Uniqueness of the Complex Numbers: Every Field Generated over an Embedded Copy of the Reals by a Square Root of -1 Is Uniquely Isomorphic to C

Each result cited is universally quantified over the data in its own statement.

Arithmetic used. $K$ is a commutative ring by Fields §field, and so is $\mathbb{C}$ by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §complex and Fields §field; in both, the laws of Commutative Rings §ring (the ring laws) and the rules Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §zero and Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs hold, and from the latter and commutativity $x\cdot(-y)=-(x\cdot y)$ (the sign rule). In $\mathbb{R}$ the rules of Rules of Arithmetic and Order in an Ordered Field hold, and real sums, products and differences agree with those formed in $\mathbb{C}$ by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §agreement.

Properties of $\lambda$. Since $\lambda(0)=\lambda(0+0)=\lambda(0)+\lambda(0)$, adding $-\lambda(0)$ to both sides gives $0_K=\lambda(0)$ by the ring laws and Negatives, Differences, Reciprocals and Quotients §negative. For $a,b\in\mathbb{R}$, $\lambda(a)+\lambda(-a)=\lambda(a+(-a))=\lambda(0)=0_K$, so $\lambda(-a)=-\lambda(a)$ by Negatives, Differences, Reciprocals and Quotients §negative, and hence $\lambda(a-b)=\lambda(a)+\lambda(-b)=\lambda(a)-\lambda(b)$.

Independence. We show: if $a,b\in\mathbb{R}$ and $\lambda(a)+\lambda(b)\cdot u=0_K$, then $a=b=0$. Suppose $b\neq0$. By Negatives, Differences, Reciprocals and Quotients §negative, $\lambda(b)\cdot u=-\lambda(a)$. Since $\lambda(b^{-1})\cdot\lambda(b)=\lambda(b^{-1}b)=\lambda(1)=1_K$, where $b^{-1}b=1$ by Negatives, Differences, Reciprocals and Quotients §reciprocal and commutativity, the ring laws and the sign rule give $u=\lambda(b^{-1})\cdot(\lambda(b)\cdot u)=\lambda(b^{-1})\cdot(-\lambda(a))=-\lambda(b^{-1}a)=\lambda(c)$ with $c=-(b^{-1}a)\in\mathbb{R}$. Then $-1_K=u\cdot u=\lambda(cc)$, so $\lambda(cc+1)=\lambda(cc)+\lambda(1)=-1_K+1_K=0_K=\lambda(0)$, and $cc+1=0$ by injectivity of $\lambda$. But $0\le cc$ and $0<1$ by Rules of Arithmetic and Order in an Ordered Field §squares, and $1\le1$ by reflexivity of the order (Partial and Total Orders on a Set and the Associated Strict Relation §partial), so $1=0+1\le cc+1=0$ by Rules of Arithmetic and Order in an Ordered Field §order-sum, contradicting $0<1$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §total-negation, the order of $\mathbb{R}$ being total since $\mathbb{R}$ is an ordered field by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals and the order of an ordered field is total by Ordered Fields. Hence $b=0$, so $\lambda(b)\cdot u=0_K\cdot u=0_K$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §zero, whence $\lambda(a)=0_K=\lambda(0)$ and $a=0$ by injectivity.

Arithmetic of $a+bi$. For $a,b,c,d\in\mathbb{R}$, the ring laws in $\mathbb{C}$ give $(a+bi)+(c+di)=(a+c)+(b+d)i$, and, with $i\cdot i=-1$ from The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §canonical and the sign rule, $(a+bi)(c+di)=ac+bd(i\cdot i)+(ad+bc)i=(ac-bd)+(ad+bc)i$. Also $a=a+0i$ and $i=0+1i$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §zero and the ring laws.

Existence. By Maps and Relations Given by Formulas §binary there are maps $g:\mathbb{R}\times\mathbb{R}\to\mathbb{C}$ with $g((a,b))=a+bi$ and $h:\mathbb{R}\times\mathbb{R}\to K$ with $h((a,b))=\lambda(a)+\lambda(b)\cdot u$. By The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §canonical, $g$ is surjective and injective (existence, respectively uniqueness, of the pair), so bijective by Injective, Surjective and Bijective Functions between Classes §bijective; by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, $\varphi=h\circ g^{-1}:\mathbb{C}\to K$ is a map with $\varphi(a+bi)=h(g^{-1}(g((a,b))))=\lambda(a)+\lambda(b)\cdot u$ for all $a,b\in\mathbb{R}$, using Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity. $g$ is only a device; no complex number is used as a pair. Let $z=a+bi$ and $w=c+di$ in $\mathbb{C}$, with $a,b,c,d\in\mathbb{R}$. By the arithmetic of $a+bi$ and the ring laws in $K$, $\varphi(z+w)=(\lambda(a)+\lambda(c))+(\lambda(b)+\lambda(d))\cdot u=\varphi(z)+\varphi(w)$. Writing $\lambda_{a}$ for $\lambda(a)$ and so on, the ring laws, $u\cdot u=-1_K$ and the sign rule give

$$\varphi(z)\cdot\varphi(w)=\lambda_{a}\lambda_{c}+\lambda_{b}\lambda_{d}(u\cdot u)+(\lambda_{a}\lambda_{d}+\lambda_{b}\lambda_{c})\cdot u=(\lambda_{a}\lambda_{c}-\lambda_{b}\lambda_{d})+(\lambda_{a}\lambda_{d}+\lambda_{b}\lambda_{c})\cdot u,$$

which is $\lambda(ac-bd)+\lambda(ad+bc)\cdot u=\varphi(zw)$ by the properties of $\lambda$ and the arithmetic of $a+bi$. For $a\in\mathbb{R}$, $\varphi(a)=\varphi(a+0i)=\lambda(a)+0_K\cdot u=\lambda(a)$, and $\varphi(i)=\varphi(0+1i)=0_K+1_K\cdot u=u$, by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §zero and the ring laws.

Uniqueness. Let $\psi:\mathbb{C}\to K$ preserve sums and products, agree with $\lambda$ on $\mathbb{R}$ and send $i$ to $u$. Every $z\in\mathbb{C}$ is $a+bi$ with $a,b\in\mathbb{R}$ by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §canonical, and then $\psi(z)=\psi(a)+\psi(b)\cdot\psi(i)=\lambda(a)+\lambda(b)\cdot u=\varphi(z)$. Both maps have domain $\mathbb{C}$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $\psi=\varphi$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. This proves the clause unique.

Bijectivity. Let $z=a+bi$ and $w=c+di$ in $\mathbb{C}$, with $a,b,c,d\in\mathbb{R}$, satisfy $\varphi(z)=\varphi(w)$, and put $v=(a-c)+(b-d)i$; then $v+w=z$ by the arithmetic of $a+bi$. So $\varphi(v)+\varphi(w)=\varphi(z)=\varphi(w)$, and adding $-\varphi(w)$ gives $\lambda(a-c)+\lambda(b-d)\cdot u=\varphi(v)=0_K$; by independence $a-c=0$ and $b-d=0$, so $z=w$. Thus $\varphi$ is injective by Injective, Surjective and Bijective Functions between Classes §injective. Every $x\in K$ equals $\lambda(a)+\lambda(b)\cdot u=\varphi(a+bi)$ for some $a,b\in\mathbb{R}$, by hypothesis, so $\varphi$ is surjective by Injective, Surjective and Bijective Functions between Classes §surjective, and bijective by Injective, Surjective and Bijective Functions between Classes §bijective.

Inverse. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, $\varphi^{-1}:K\to\mathbb{C}$ is a map with $\varphi^{-1}(\varphi(z))=z$ for $z\in\mathbb{C}$ and $\varphi(\varphi^{-1}(x))=x$ for $x\in K$. For $x,y\in K$, $\varphi(\varphi^{-1}(x)+\varphi^{-1}(y))=x+y=\varphi(\varphi^{-1}(x+y))$, so $\varphi^{-1}(x+y)=\varphi^{-1}(x)+\varphi^{-1}(y)$ by injectivity of $\varphi$; likewise $\varphi^{-1}(x\cdot y)=\varphi^{-1}(x)\varphi^{-1}(y)$. Finally $\varphi^{-1}(\lambda(a))=\varphi^{-1}(\varphi(a))=a$ for $a\in\mathbb{R}$ and $\varphi^{-1}(u)=\varphi^{-1}(\varphi(i))=i$. This proves the clause isomorphism.

Two fields. Let $K'$, $\lambda'$ and $u'$ be as in the clause two-fields. The clauses unique and isomorphism, proved above for arbitrary data satisfying the hypotheses, apply to $(K,\lambda,u)$ and to $(K',\lambda',u')$: let $\varphi:\mathbb{C}\to K$ and $\varphi':\mathbb{C}\to K'$ be the maps they give. By the clause isomorphism and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, $\varphi^{-1}:K\to\mathbb{C}$ and $\varphi'^{-1}:K'\to\mathbb{C}$ are maps with $\varphi(\varphi^{-1}(x))=x$ for $x\in K$, $\varphi'^{-1}(\varphi'(z))=z$ for $z\in\mathbb{C}$, and $\varphi'(\varphi'^{-1}(x'))=x'$ for $x'\in K'$, and they preserve sums and products. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, $\psi=\varphi'\circ\varphi^{-1}:K\to K'$ is a map with $\psi(x)=\varphi'(\varphi^{-1}(x))$. For $x,y\in K$, $\psi(x+y)=\varphi'(\varphi^{-1}(x)+\varphi^{-1}(y))=\psi(x)+\psi(y)$ and likewise $\psi(x\cdot y)=\psi(x)\cdot\psi(y)$; for $a\in\mathbb{R}$, $\psi(\lambda(a))=\varphi'(\varphi^{-1}(\lambda(a)))=\varphi'(a)=\lambda'(a)$; and $\psi(u)=\varphi'(\varphi^{-1}(u))=\varphi'(i)=u'$. So $\psi$ has the stated properties.

Let $\chi:K\to K'$ be any map with these properties. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, $\chi\circ\varphi:\mathbb{C}\to K'$ is a map with $(\chi\circ\varphi)(z)=\chi(\varphi(z))$; it preserves sums and products since $\varphi$ and $\chi$ do, $(\chi\circ\varphi)(a)=\chi(\lambda(a))=\lambda'(a)$ for $a\in\mathbb{R}$, and $(\chi\circ\varphi)(i)=\chi(u)=u'$. By the clause unique for $(K',\lambda',u')$, $\chi\circ\varphi=\varphi'$. Hence for $x\in K$, $\chi(x)=\chi(\varphi(\varphi^{-1}(x)))=\varphi'(\varphi^{-1}(x))=\psi(x)$; both maps have domain $K$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $\chi=\psi$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Thus $\psi$ is the only such map.

Exchanging the roles of $(K,\lambda,u)$ and $(K',\lambda',u')$, the argument above shows that $\psi'=\varphi\circ\varphi'^{-1}:K'\to K$ is a map with $\psi'(x'+y')=\psi'(x')+\psi'(y')$ and $\psi'(x'\cdot y')=\psi'(x')\cdot\psi'(y')$ for $x',y'\in K'$, $\psi'(\lambda'(a))=\lambda(a)$ for $a\in\mathbb{R}$, and $\psi'(u')=u$. For $x\in K$, $\psi'(\psi(x))=\varphi(\varphi'^{-1}(\varphi'(\varphi^{-1}(x))))=\varphi(\varphi^{-1}(x))=x$, and likewise $\psi(\psi'(x'))=x'$ for $x'\in K'$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, Functions, Values of a Function, and Functions from One Class to Another §map and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, $\psi'\circ\psi=\mathrm{id}_{K}$ and $\psi\circ\psi'=\mathrm{id}_{K'}$, so $\psi$ is bijective and $\psi^{-1}=\psi'$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion. Hence $\psi^{-1}$ has the stated properties. This proves the clause two-fields.