Proof of Kit for def:complex-numbers-nbg

Routine facts about sets, maps and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity): the values of the parameters are sets, elements of classes are sets (Classes, Membership, Sets and Proper Classes (i)), the one-entry tuple $\langle a\rangle$ is $a$ (The Ordered Pair of Two Sets and Nested Tuples (ii)), and a map between sets lies in the corresponding class of functions (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)). Formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi) and quantify over set variables only, so they are predicative. The parameters $\mathbb{R}$, $+$, $\cdot$ and $0$ are set variables other than $x_{0},\dots,x_{n-1}$ and other than the bound variables below. We first build formulas in the single set variable $x_{0}$, written $F$, and move them to the position $i$ at the end. The letters $a,b,c,d,e,f,g,h,q,s,t,w,w',z,p,u,u',v,v'$ denote further pairwise distinct set variables, all distinct from $F$.

Binary operations on $\mathbb{C}$. For variables $A$ and $B$ let $\pi(z,A,B)$ be the formula $\forall p\,\bigl(p\in z\Leftrightarrow\exists u\,\exists v\,(u\in A\wedge v\in B\wedge p=(u,v))\bigr)$. For sets $A$ and $B$, the only set $z$ with $\pi(z,A,B)$ is the Cartesian product $A\times B$, which is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii); and $\mathbb{C}=\mathbb{R}\times\mathbb{R}$ by The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (i). Let $\mu(F,A,B)$ be the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), with the set variables $p,u,u',v,v'$ above, which holds exactly when $F$ is a map $F:A\to B$, and let

$$\gamma=\exists w\,\bigl(\pi(w,\mathbb{R},\mathbb{R})\wedge\exists w'\,(\pi(w',w,w)\wedge\mu(F,w',w))\bigr).$$

By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii), applied first to $w'$, for every set $w$, and then to $w$, the formula $\gamma$ holds exactly when $\mu(F,\mathbb{C}\times\mathbb{C},\mathbb{C})$ does, that is, exactly when $F$ is a map $F:\mathbb{C}\times\mathbb{C}\to\mathbb{C}$, a binary operation on $\mathbb{C}$.

Assume $\gamma$. Throughout, that pairs of elements of $\mathbb{R}$ lie in $\mathbb{C}$ and pairs of elements of $\mathbb{C}$ in $\mathbb{C}\times\mathbb{C}$, that pairs are sets, and that the values of $+$ and $\cdot$ at elements of $\mathbb{R}$ lie in $\mathbb{R}$, are routine facts of the setting. For $a,b,c,d,r,r'\in\mathbb{R}$ and every set $y$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), $(((a,b),(c,d)),y)\in F$ holds exactly for $y=(a,b)\mathbin{F}(c,d)$, the value of $F$ at $((a,b),(c,d))$, and $((r,r'),y)\in{+}$ and $((r,r'),y)\in{\cdot}$ hold exactly for $y=r+r'$ and $y=r\cdot r'$. For $r\in\mathbb{R}$, the conditions $y\in\mathbb{R}$ and $((r,y),0)\in{+}$ hold together exactly for $y=-r$, and $r'-r=r'+(-r)$, by Negatives, Differences, Reciprocals and Quotients (i). So in each formula below every premise of these forms singles out exactly one set, which exists, and a universally quantified implication whose premises name values in this way states the property of the named values given in its conclusion (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii)).

The values. Let $\alpha_{+}$ and $\alpha_{\cdot}$ be the formulas

$$\begin{aligned} &\forall a\,\forall b\,\forall c\,\forall d\,\forall s\,\forall t\,\bigl((a\in\mathbb{R}\wedge b\in\mathbb{R}\wedge c\in\mathbb{R}\wedge d\in\mathbb{R}\wedge((a,c),s)\in{+}\wedge((b,d),t)\in{+})\Rightarrow(((a,b),(c,d)),(s,t))\in F\bigr),\\ &\forall a\,\forall b\,\forall c\,\forall d\,\forall e\,\forall f\,\forall q\,\forall g\,\forall h\,\forall s\,\forall t\,\bigl((a\in\mathbb{R}\wedge b\in\mathbb{R}\wedge c\in\mathbb{R}\wedge d\in\mathbb{R}\wedge((a,c),e)\in{\cdot}\wedge((b,d),f)\in{\cdot}\wedge q\in\mathbb{R}\wedge((f,q),0)\in{+}\\ &\qquad\wedge((e,q),s)\in{+}\wedge((a,d),g)\in{\cdot}\wedge((b,c),h)\in{\cdot}\wedge((g,h),t)\in{+})\Rightarrow(((a,b),(c,d)),(s,t))\in F\bigr). \end{aligned}$$

Under $\gamma$ their premises name $s=a+c$ and $t=b+d$ in the first; and $e=ac$, $f=bd$, $q=-bd$, $s=ac+(-bd)=ac-bd$, $g=ad$, $h=bc$ and $t=ad+bc$ in the second. The conclusion says that the pair $(s,t)$ is the value $(a,b)\mathbin{F}(c,d)$. So, under $\gamma$, $\alpha_{+}$ and $\alpha_{\cdot}$ state, respectively,

$$(a,b)\mathbin{F}(c,d)=(a+c,\,b+d)\qquad\text{and}\qquad(a,b)\mathbin{F}(c,d)=(ac-bd,\,ad+bc)\qquad\text{for all }a,b,c,d\in\mathbb{R}.$$

The sum and the product. Let $\varphi_{+}=\gamma\wedge\alpha_{+}$ and $\varphi_{\cdot}=\gamma\wedge\alpha_{\cdot}$. By The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii), the sum operation of $\mathbb{C}$ is a binary operation on $\mathbb{C}$ satisfying the first displayed identity, so $\varphi_{+}$ holds when $F$ is assigned it. Conversely, let $F$ be a set satisfying $\varphi_{+}$. Every element of $\mathbb{C}\times\mathbb{C}$ is a pair of elements of $\mathbb{C}$ (The Cartesian Product of Two Classes (i)), and every element of $\mathbb{C}$ is a pair $(a,b)$ with $a,b\in\mathbb{R}$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (ii)); so $F$ and the sum operation are maps $\mathbb{C}\times\mathbb{C}\to\mathbb{C}$ with the same value $(a+c,b+d)$ at every element $((a,b),(c,d))$ of $\mathbb{C}\times\mathbb{C}$. Two maps with the same domain and the same values are equal by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii), so $F$ is the sum operation of $\mathbb{C}$. Thus $\varphi_{+}$ holds exactly when $F$ is the sum operation of $\mathbb{C}$; in the same way, with the values $(ac-bd,ad+bc)$, $\varphi_{\cdot}$ holds exactly when $F$ is the product operation of $\mathbb{C}$. Each of $\varphi_{+}$ and $\varphi_{\cdot}$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), and is therefore a predicative formula in $x_{0}$ in the sense of Renaming and Substituting Variables in Predicative Formulas, with parameters among $\mathbb{R}$, $+$, $\cdot$ and $0$.

Any position. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$ (the given $x_{0},\dots,x_{n-1}$ being the first of the distinct set variables $x_{0},x_{1},\dots$ there), the formulas $\varphi_{+}(x_{i})$ and $\varphi_{\cdot}(x_{i})$ are predicative formulas in $x_{0},\dots,x_{n-1}$ that hold, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $\varphi_{+}$, respectively $\varphi_{\cdot}$, holds with $x_{0}$ assigned the set assigned to $x_{i}$, that is, exactly when $x_{i}$ is the sum operation, respectively the product operation, of $\mathbb{C}$. This proves (i) and (ii).

The classes. The Class Comprehension Theorem for Predicative Formulas (i), applied to $\varphi_{+}$, respectively $\varphi_{\cdot}$, with $x_{0}$ as its single variable and $\mathbb{R}$, $+$, $\cdot$ and $0$ as its parameters, gives a class whose set elements are exactly the sets that are the sum operation, respectively the product operation, of $\mathbb{C}$. Since every element of a class is a set, and so is each of these operations, a map between the sets $\mathbb{C}\times\mathbb{C}$ and $\mathbb{C}$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii), Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii)), this class serves as the $A$ of (iii), respectively the $M$ of (iv).