df-bj-addc - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-addc		Structured version Visualization version GIF version

Definition df-bj-addc 38299

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). We use the plural in "additions" since these are two different operations, even though +_ℂ̅ is overloaded. (Contributed by BJ, 22-Jun-2019.)

**Assertion**
Ref	Expression
df-bj-addc	⊢ +_ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ_∞))) ↦ if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if((1^st ‘𝑥) ∈ ℂ, if((2^nd ‘𝑥) ∈ ℂ, ⟨((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥))), ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))⟩, (2^nd ‘𝑥)), (1^st ‘𝑥))))

**Detailed syntax breakdown of Definition df-bj-addc**
Step	Hyp	Ref	Expression
1		caddcc 38298	. 2 class +_ℂ̅
2		vx	. . 3 setvar 𝑥
3		cc 11208	. . . . . 6 class ℂ
4		cccbar 38276	. . . . . 6 class ℂ̅
5	3, 4	cxp 5652	. . . . 5 class (ℂ × ℂ̅)
6	4, 3	cxp 5652	. . . . 5 class (ℂ̅ × ℂ)
7	5, 6	cun 4151	. . . 4 class ((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ))
8		ccchat 38293	. . . . . 6 class ℂ̂
9	8, 8	cxp 5652	. . . . 5 class (ℂ̂ × ℂ̂)
10		cid 5548	. . . . . 6 class I
11		cccinfty 38272	. . . . . 6 class ℂ_∞
12	10, 11	cres 5656	. . . . 5 class ( I ↾ ℂ_∞)
13	9, 12	cun 4151	. . . 4 class ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ_∞))
14	7, 13	cun 4151	. . 3 class (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ_∞)))
15	2	cv 1568	. . . . . . 7 class 𝑥
16		c1st 8006	. . . . . . 7 class 1^st
17	15, 16	cfv 6546	. . . . . 6 class (1^st ‘𝑥)
18		cinfty 38291	. . . . . 6 class ∞
19	17, 18	wceq 1569	. . . . 5 wff (1^st ‘𝑥) = ∞
20		c2nd 8007	. . . . . . 7 class 2^nd
21	15, 20	cfv 6546	. . . . . 6 class (2^nd ‘𝑥)
22	21, 18	wceq 1569	. . . . 5 wff (2^nd ‘𝑥) = ∞
23	19, 22	wo 861	. . . 4 wff ((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞)
24	17, 3	wcel 2146	. . . . 5 wff (1^st ‘𝑥) ∈ ℂ
25	21, 3	wcel 2146	. . . . . 6 wff (2^nd ‘𝑥) ∈ ℂ
26	17, 16	cfv 6546	. . . . . . . 8 class (1^st ‘(1^st ‘𝑥))
27	21, 16	cfv 6546	. . . . . . . 8 class (1^st ‘(2^nd ‘𝑥))
28		cplr 10964	. . . . . . . 8 class +_R
29	26, 27, 28	co 7427	. . . . . . 7 class ((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥)))
30	17, 20	cfv 6546	. . . . . . . 8 class (2^nd ‘(1^st ‘𝑥))
31	21, 20	cfv 6546	. . . . . . . 8 class (2^nd ‘(2^nd ‘𝑥))
32	30, 31, 28	co 7427	. . . . . . 7 class ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))
33	29, 32	cop 4837	. . . . . 6 class ⟨((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥))), ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))⟩
34	25, 33, 21	cif 4484	. . . . 5 class if((2^nd ‘𝑥) ∈ ℂ, ⟨((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥))), ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))⟩, (2^nd ‘𝑥))
35	24, 34, 17	cif 4484	. . . 4 class if((1^st ‘𝑥) ∈ ℂ, if((2^nd ‘𝑥) ∈ ℂ, ⟨((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥))), ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))⟩, (2^nd ‘𝑥)), (1^st ‘𝑥))
36	23, 18, 35	cif 4484	. . 3 class if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if((1^st ‘𝑥) ∈ ℂ, if((2^nd ‘𝑥) ∈ ℂ, ⟨((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥))), ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))⟩, (2^nd ‘𝑥)), (1^st ‘𝑥)))
37	2, 14, 36	cmpt 5188	. 2 class (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ_∞))) ↦ if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if((1^st ‘𝑥) ∈ ℂ, if((2^nd ‘𝑥) ∈ ℂ, ⟨((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥))), ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))⟩, (2^nd ‘𝑥)), (1^st ‘𝑥))))
38	1, 37	wceq 1569	1 wff +_ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ_∞))) ↦ if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if((1^st ‘𝑥) ∈ ℂ, if((2^nd ‘𝑥) ∈ ℂ, ⟨((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥))), ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))⟩, (2^nd ‘𝑥)), (1^st ‘𝑥))))

Colors of variables: wff setvar class

This definition is used by: (None)

W3C validator