Definition df-bj-addc 32302

Description: Define the additions on the extended complex numbers (on the subset of (ℂ̅ × ℂ̅) where it makes sense) and on the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-bj-addc	⊢ +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥))))

Detailed syntax breakdown of Definition df-bj-addc

Step	Hyp	Ref	Expression
1		caddcc 32301	. 2 class +ℂ̅
2		vx	. . 3 setvar 𝑥
3		cc 9813	. . . . . 6 class ℂ
4		cccbar 32279	. . . . . 6 class ℂ̅
5	3, 4	cxp 5036	. . . . 5 class (ℂ × ℂ̅)
6	4, 3	cxp 5036	. . . . 5 class (ℂ̅ × ℂ)
7	5, 6	cun 3538	. . . 4 class ((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ))
8		ccchat 32296	. . . . . 6 class ℂ̂
9	8, 8	cxp 5036	. . . . 5 class (ℂ̂ × ℂ̂)
10		cccinfty 32275	. . . . . 6 class ℂ∞
11		cdiag2 32265	. . . . . 6 class Diag
12	10, 11	cfv 5804	. . . . 5 class (Diag‘ℂ∞)
13	9, 12	cun 3538	. . . 4 class ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))
14	7, 13	cun 3538	. . 3 class (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞)))
15	2	cv 1474	. . . . . . 7 class 𝑥
16		c1st 7057	. . . . . . 7 class 1st
17	15, 16	cfv 5804	. . . . . 6 class (1st ‘𝑥)
18		cinfty 32294	. . . . . 6 class ∞
19	17, 18	wceq 1475	. . . . 5 wff (1st ‘𝑥) = ∞
20		c2nd 7058	. . . . . . 7 class 2nd
21	15, 20	cfv 5804	. . . . . 6 class (2nd ‘𝑥)
22	21, 18	wceq 1475	. . . . 5 wff (2nd ‘𝑥) = ∞
23	19, 22	wo 382	. . . 4 wff ((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞)
24	17, 3	wcel 1977	. . . . 5 wff (1st ‘𝑥) ∈ ℂ
25	21, 3	wcel 1977	. . . . . 6 wff (2nd ‘𝑥) ∈ ℂ
26		caddc 9818	. . . . . . 7 class +
27	17, 21, 26	co 6549	. . . . . 6 class ((1st ‘𝑥) + (2nd ‘𝑥))
28	25, 27, 21	cif 4036	. . . . 5 class if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥))
29	24, 28, 17	cif 4036	. . . 4 class if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥))
30	23, 18, 29	cif 4036	. . 3 class if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥)))
31	2, 14, 30	cmpt 4643	. 2 class (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥))))
32	1, 31	wceq 1475	1 wff +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥))))

This definition is referenced by: (None)