Definition df-bj-addc

Description: Define the additions on the extended complex numbers (on the subset of ( CCbar X. CCbar ) where it makes sense) and on the complex projective line (Riemann sphere). We use the plural in "additions" since these are two different operations, even though +cc is overloaded. (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	df-bj-addc	$$⊢{+}_{\overline{ℂ}}=\left(x\in \left(\left(\left(ℂ\times \overline{ℂ}\right)\cup \left(\overline{ℂ}\times ℂ\right)\right)\cup \left(\left(\widehat{ℂ}\times \widehat{ℂ}\right)\cup \left({\mathrm{I}\upharpoonright }_{{ℂ}_{\infty }}\right)\right)\right)⟼if\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(1^{st}\left(x\right)\in ℂ,if\left(2^{nd}\left(x\right)\in ℂ,⟨1^{st}\left(1^{st}\left(x\right)\right){+}_{𝑹}{1}^{st}\left(2^{nd}\left(x\right)\right),2^{nd}\left(1^{st}\left(x\right)\right){+}_{𝑹}{2}^{nd}\left(2^{nd}\left(x\right)\right)⟩,2^{nd}\left(x\right)\right),1^{st}\left(x\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caddcc	$$class{+}_{\overline{ℂ}}$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		cccbar	$$class\overline{ℂ}$$
4	2 3	cxp	$$class\left(ℂ\times \overline{ℂ}\right)$$
5	3 2	cxp	$$class\left(\overline{ℂ}\times ℂ\right)$$
6	4 5	cun	$$class\left(\left(ℂ\times \overline{ℂ}\right)\cup \left(\overline{ℂ}\times ℂ\right)\right)$$
7		ccchat	$$class\widehat{ℂ}$$
8	7 7	cxp	$$class\left(\widehat{ℂ}\times \widehat{ℂ}\right)$$
9		cid	$$class\mathrm{I}$$
10		cccinfty	$$class{ℂ}_{\infty }$$
11	9 10	cres	$$class\left({\mathrm{I}\upharpoonright }_{{ℂ}_{\infty }}\right)$$
12	8 11	cun	$$class\left(\left(\widehat{ℂ}\times \widehat{ℂ}\right)\cup \left({\mathrm{I}\upharpoonright }_{{ℂ}_{\infty }}\right)\right)$$
13	6 12	cun	$$class\left(\left(\left(ℂ\times \overline{ℂ}\right)\cup \left(\overline{ℂ}\times ℂ\right)\right)\cup \left(\left(\widehat{ℂ}\times \widehat{ℂ}\right)\cup \left({\mathrm{I}\upharpoonright }_{{ℂ}_{\infty }}\right)\right)\right)$$
14		c1st	$$class{1}^{st}$$
15	1	cv	$$setvarx$$
16	15 14	cfv	$$class{1}^{st}\left(x\right)$$
17		cinfty	$$class\infty$$
18	16 17	wceq	$$wff{1}^{st}\left(x\right)=\infty$$
19		c2nd	$$class{2}^{nd}$$
20	15 19	cfv	$$class{2}^{nd}\left(x\right)$$
21	20 17	wceq	$$wff{2}^{nd}\left(x\right)=\infty$$
22	18 21	wo	$$wff\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right)$$
23	16 2	wcel	$$wff{1}^{st}\left(x\right)\in ℂ$$
24	20 2	wcel	$$wff{2}^{nd}\left(x\right)\in ℂ$$
25	16 14	cfv	$$class{1}^{st}\left(1^{st}\left(x\right)\right)$$
26		cplr	$$class{+}_{𝑹}$$
27	20 14	cfv	$$class{1}^{st}\left(2^{nd}\left(x\right)\right)$$
28	25 27 26	co	$$class\left(1^{st}\left(1^{st}\left(x\right)\right){+}_{𝑹}{1}^{st}\left(2^{nd}\left(x\right)\right)\right)$$
29	16 19	cfv	$$class{2}^{nd}\left(1^{st}\left(x\right)\right)$$
30	20 19	cfv	$$class{2}^{nd}\left(2^{nd}\left(x\right)\right)$$
31	29 30 26	co	$$class\left(2^{nd}\left(1^{st}\left(x\right)\right){+}_{𝑹}{2}^{nd}\left(2^{nd}\left(x\right)\right)\right)$$
32	28 31	cop	$$class⟨1^{st}\left(1^{st}\left(x\right)\right){+}_{𝑹}{1}^{st}\left(2^{nd}\left(x\right)\right),2^{nd}\left(1^{st}\left(x\right)\right){+}_{𝑹}{2}^{nd}\left(2^{nd}\left(x\right)\right)⟩$$
33	24 32 20	cif	$$classif\left(2^{nd}\left(x\right)\in ℂ,⟨1^{st}\left(1^{st}\left(x\right)\right){+}_{𝑹}{1}^{st}\left(2^{nd}\left(x\right)\right),2^{nd}\left(1^{st}\left(x\right)\right){+}_{𝑹}{2}^{nd}\left(2^{nd}\left(x\right)\right)⟩,2^{nd}\left(x\right)\right)$$
34	23 33 16	cif	$$classif\left(1^{st}\left(x\right)\in ℂ,if\left(2^{nd}\left(x\right)\in ℂ,⟨1^{st}\left(1^{st}\left(x\right)\right){+}_{𝑹}{1}^{st}\left(2^{nd}\left(x\right)\right),2^{nd}\left(1^{st}\left(x\right)\right){+}_{𝑹}{2}^{nd}\left(2^{nd}\left(x\right)\right)⟩,2^{nd}\left(x\right)\right),1^{st}\left(x\right)\right)$$
35	22 17 34	cif	$$classif\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(1^{st}\left(x\right)\in ℂ,if\left(2^{nd}\left(x\right)\in ℂ,⟨1^{st}\left(1^{st}\left(x\right)\right){+}_{𝑹}{1}^{st}\left(2^{nd}\left(x\right)\right),2^{nd}\left(1^{st}\left(x\right)\right){+}_{𝑹}{2}^{nd}\left(2^{nd}\left(x\right)\right)⟩,2^{nd}\left(x\right)\right),1^{st}\left(x\right)\right)\right)$$
36	1 13 35	cmpt	$$class\left(x\in \left(\left(\left(ℂ\times \overline{ℂ}\right)\cup \left(\overline{ℂ}\times ℂ\right)\right)\cup \left(\left(\widehat{ℂ}\times \widehat{ℂ}\right)\cup \left({\mathrm{I}\upharpoonright }_{{ℂ}_{\infty }}\right)\right)\right)⟼if\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(1^{st}\left(x\right)\in ℂ,if\left(2^{nd}\left(x\right)\in ℂ,⟨1^{st}\left(1^{st}\left(x\right)\right){+}_{𝑹}{1}^{st}\left(2^{nd}\left(x\right)\right),2^{nd}\left(1^{st}\left(x\right)\right){+}_{𝑹}{2}^{nd}\left(2^{nd}\left(x\right)\right)⟩,2^{nd}\left(x\right)\right),1^{st}\left(x\right)\right)\right)\right)$$
37	0 36	wceq	$$wff{+}_{\overline{ℂ}}=\left(x\in \left(\left(\left(ℂ\times \overline{ℂ}\right)\cup \left(\overline{ℂ}\times ℂ\right)\right)\cup \left(\left(\widehat{ℂ}\times \widehat{ℂ}\right)\cup \left({\mathrm{I}\upharpoonright }_{{ℂ}_{\infty }}\right)\right)\right)⟼if\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(1^{st}\left(x\right)\in ℂ,if\left(2^{nd}\left(x\right)\in ℂ,⟨1^{st}\left(1^{st}\left(x\right)\right){+}_{𝑹}{1}^{st}\left(2^{nd}\left(x\right)\right),2^{nd}\left(1^{st}\left(x\right)\right){+}_{𝑹}{2}^{nd}\left(2^{nd}\left(x\right)\right)⟩,2^{nd}\left(x\right)\right),1^{st}\left(x\right)\right)\right)\right)$$