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	⊢ +_ℂ̅ = ( 𝑥 ∈ ( ( ( ℂ × ℂ̅ ) ∪ ( ℂ̅ × ℂ ) ) ∪ ( ( ℂ̂ × ℂ̂ ) ∪ ( 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

Step	Hyp	Ref	Expression
0		caddcc	⊢ +_ℂ̅
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		cccbar	⊢ ℂ̅
4	2 3	cxp	⊢ ( ℂ × ℂ̅ )
5	3 2	cxp	⊢ ( ℂ̅ × ℂ )
6	4 5	cun	⊢ ( ( ℂ × ℂ̅ ) ∪ ( ℂ̅ × ℂ ) )
7		ccchat	⊢ ℂ̂
8	7 7	cxp	⊢ ( ℂ̂ × ℂ̂ )
9		cid	⊢ I
10		cccinfty	⊢ ℂ_∞
11	9 10	cres	⊢ ( I ↾ ℂ_∞ )
12	8 11	cun	⊢ ( ( ℂ̂ × ℂ̂ ) ∪ ( I ↾ ℂ_∞ ) )
13	6 12	cun	⊢ ( ( ( ℂ × ℂ̅ ) ∪ ( ℂ̅ × ℂ ) ) ∪ ( ( ℂ̂ × ℂ̂ ) ∪ ( I ↾ ℂ_∞ ) ) )
14		c1st	⊢ 1^st
15	1	cv	⊢ 𝑥
16	15 14	cfv	⊢ ( 1^st ‘ 𝑥 )
17		cinfty	⊢ ∞
18	16 17	wceq	⊢ ( 1^st ‘ 𝑥 ) = ∞
19		c2nd	⊢ 2^nd
20	15 19	cfv	⊢ ( 2^nd ‘ 𝑥 )
21	20 17	wceq	⊢ ( 2^nd ‘ 𝑥 ) = ∞
22	18 21	wo	⊢ ( ( 1^st ‘ 𝑥 ) = ∞ ∨ ( 2^nd ‘ 𝑥 ) = ∞ )
23	16 2	wcel	⊢ ( 1^st ‘ 𝑥 ) ∈ ℂ
24	20 2	wcel	⊢ ( 2^nd ‘ 𝑥 ) ∈ ℂ
25	16 14	cfv	⊢ ( 1^st ‘ ( 1^st ‘ 𝑥 ) )
26		cplr	⊢ +_R
27	20 14	cfv	⊢ ( 1^st ‘ ( 2^nd ‘ 𝑥 ) )
28	25 27 26	co	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) +_R ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) )
29	16 19	cfv	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) )
30	20 19	cfv	⊢ ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) )
31	29 30 26	co	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) +_R ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) )
32	28 31	cop	⊢ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) +_R ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) +_R ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) ⟩
33	24 32 20	cif	⊢ if ( ( 2^nd ‘ 𝑥 ) ∈ ℂ , ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) +_R ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) +_R ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) ⟩ , ( 2^nd ‘ 𝑥 ) )
34	23 33 16	cif	⊢ 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 ‘ 𝑥 ) )
35	22 17 34	cif	⊢ 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 ‘ 𝑥 ) ) )
36	1 13 35	cmpt	⊢ ( 𝑥 ∈ ( ( ( ℂ × ℂ̅ ) ∪ ( ℂ̅ × ℂ ) ) ∪ ( ( ℂ̂ × ℂ̂ ) ∪ ( 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 ‘ 𝑥 ) ) ) )
37	0 36	wceq	⊢ +_ℂ̅ = ( 𝑥 ∈ ( ( ( ℂ × ℂ̅ ) ∪ ( ℂ̅ × ℂ ) ) ∪ ( ( ℂ̂ × ℂ̂ ) ∪ ( 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 ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Definition df-bj-addc

Detailed syntax breakdown