Definition df-bj-addc 33125

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 33124	. 2 class +ℂ̅
2		vx	. . 3 setvar 𝑥
3		cc 9934	. . . . . 6 class ℂ
4		cccbar 33102	. . . . . 6 class ℂ̅
5	3, 4	cxp 5112	. . . . 5 class (ℂ × ℂ̅)
6	4, 3	cxp 5112	. . . . 5 class (ℂ̅ × ℂ)
7	5, 6	cun 3572	. . . 4 class ((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ))
8		ccchat 33119	. . . . . 6 class ℂ̂
9	8, 8	cxp 5112	. . . . 5 class (ℂ̂ × ℂ̂)
10		cccinfty 33098	. . . . . 6 class ℂ∞
11		cdiag2 33088	. . . . . 6 class Diag
12	10, 11	cfv 5888	. . . . 5 class (Diag‘ℂ∞)
13	9, 12	cun 3572	. . . 4 class ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))
14	7, 13	cun 3572	. . 3 class (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞)))
15	2	cv 1482	. . . . . . 7 class 𝑥
16		c1st 7166	. . . . . . 7 class 1st
17	15, 16	cfv 5888	. . . . . 6 class (1st ‘𝑥)
18		cinfty 33117	. . . . . 6 class ∞
19	17, 18	wceq 1483	. . . . 5 wff (1st ‘𝑥) = ∞
20		c2nd 7167	. . . . . . 7 class 2nd
21	15, 20	cfv 5888	. . . . . 6 class (2nd ‘𝑥)
22	21, 18	wceq 1483	. . . . 5 wff (2nd ‘𝑥) = ∞
23	19, 22	wo 383	. . . 4 wff ((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞)
24	17, 3	wcel 1990	. . . . 5 wff (1st ‘𝑥) ∈ ℂ
25	21, 3	wcel 1990	. . . . . 6 wff (2nd ‘𝑥) ∈ ℂ
26		caddc 9939	. . . . . . 7 class +
27	17, 21, 26	co 6650	. . . . . 6 class ((1st ‘𝑥) + (2nd ‘𝑥))
28	25, 27, 21	cif 4086	. . . . 5 class if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥))
29	24, 28, 17	cif 4086	. . . 4 class if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥))
30	23, 18, 29	cif 4086	. . 3 class if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥)))
31	2, 14, 30	cmpt 4729	. 2 class (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥))))
32	1, 31	wceq 1483	1 wff +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥))))

This definition is referenced by: (None)