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 35336

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 35335	. 2 class +_ℂ̅
2		vx	. . 3 setvar 𝑥
3		cc 10800	. . . . . 6 class ℂ
4		cccbar 35313	. . . . . 6 class ℂ̅
5	3, 4	cxp 5578	. . . . 5 class (ℂ × ℂ̅)
6	4, 3	cxp 5578	. . . . 5 class (ℂ̅ × ℂ)
7	5, 6	cun 3881	. . . 4 class ((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ))
8		ccchat 35330	. . . . . 6 class ℂ̂
9	8, 8	cxp 5578	. . . . 5 class (ℂ̂ × ℂ̂)
10		cid 5479	. . . . . 6 class I
11		cccinfty 35309	. . . . . 6 class ℂ_∞
12	10, 11	cres 5582	. . . . 5 class ( I ↾ ℂ_∞)
13	9, 12	cun 3881	. . . 4 class ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ_∞))
14	7, 13	cun 3881	. . 3 class (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ_∞)))
15	2	cv 1538	. . . . . . 7 class 𝑥
16		c1st 7802	. . . . . . 7 class 1^st
17	15, 16	cfv 6418	. . . . . 6 class (1^st ‘𝑥)
18		cinfty 35328	. . . . . 6 class ∞
19	17, 18	wceq 1539	. . . . 5 wff (1^st ‘𝑥) = ∞
20		c2nd 7803	. . . . . . 7 class 2^nd
21	15, 20	cfv 6418	. . . . . 6 class (2^nd ‘𝑥)
22	21, 18	wceq 1539	. . . . 5 wff (2^nd ‘𝑥) = ∞
23	19, 22	wo 843	. . . 4 wff ((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞)
24	17, 3	wcel 2108	. . . . 5 wff (1^st ‘𝑥) ∈ ℂ
25	21, 3	wcel 2108	. . . . . 6 wff (2^nd ‘𝑥) ∈ ℂ
26	17, 16	cfv 6418	. . . . . . . 8 class (1^st ‘(1^st ‘𝑥))
27	21, 16	cfv 6418	. . . . . . . 8 class (1^st ‘(2^nd ‘𝑥))
28		cplr 10556	. . . . . . . 8 class +_R
29	26, 27, 28	co 7255	. . . . . . 7 class ((1^st ‘(1^st ‘𝑥)) +_R (1^st ‘(2^nd ‘𝑥)))
30	17, 20	cfv 6418	. . . . . . . 8 class (2^nd ‘(1^st ‘𝑥))
31	21, 20	cfv 6418	. . . . . . . 8 class (2^nd ‘(2^nd ‘𝑥))
32	30, 31, 28	co 7255	. . . . . . 7 class ((2^nd ‘(1^st ‘𝑥)) +_R (2^nd ‘(2^nd ‘𝑥)))
33	29, 32	cop 4564	. . . . . 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 4456	. . . . 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 4456	. . . 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 4456	. . 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 5153	. 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 1539	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 referenced by: (None)

W3C validator