Users' Mathboxes 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 34412
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(((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞), ∞, if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ⟨((1st ‘(1st𝑥)) +R (1st ‘(2nd𝑥))), ((2nd ‘(1st𝑥)) +R (2nd ‘(2nd𝑥)))⟩, (2nd𝑥)), (1st𝑥))))

Detailed syntax breakdown of Definition df-bj-addc
StepHypRef Expression
1 caddcc 34411 . 2 class +ℂ̅
2 vx . . 3 setvar 𝑥
3 cc 10523 . . . . . 6 class
4 cccbar 34389 . . . . . 6 class ℂ̅
53, 4cxp 5546 . . . . 5 class (ℂ × ℂ̅)
64, 3cxp 5546 . . . . 5 class (ℂ̅ × ℂ)
75, 6cun 3931 . . . 4 class ((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ))
8 ccchat 34406 . . . . . 6 class ℂ̂
98, 8cxp 5546 . . . . 5 class (ℂ̂ × ℂ̂)
10 cid 5452 . . . . . 6 class I
11 cccinfty 34385 . . . . . 6 class
1210, 11cres 5550 . . . . 5 class ( I ↾ ℂ)
139, 12cun 3931 . . . 4 class ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ))
147, 13cun 3931 . . 3 class (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ)))
152cv 1527 . . . . . . 7 class 𝑥
16 c1st 7676 . . . . . . 7 class 1st
1715, 16cfv 6348 . . . . . 6 class (1st𝑥)
18 cinfty 34404 . . . . . 6 class
1917, 18wceq 1528 . . . . 5 wff (1st𝑥) = ∞
20 c2nd 7677 . . . . . . 7 class 2nd
2115, 20cfv 6348 . . . . . 6 class (2nd𝑥)
2221, 18wceq 1528 . . . . 5 wff (2nd𝑥) = ∞
2319, 22wo 841 . . . 4 wff ((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞)
2417, 3wcel 2105 . . . . 5 wff (1st𝑥) ∈ ℂ
2521, 3wcel 2105 . . . . . 6 wff (2nd𝑥) ∈ ℂ
2617, 16cfv 6348 . . . . . . . 8 class (1st ‘(1st𝑥))
2721, 16cfv 6348 . . . . . . . 8 class (1st ‘(2nd𝑥))
28 cplr 10279 . . . . . . . 8 class +R
2926, 27, 28co 7145 . . . . . . 7 class ((1st ‘(1st𝑥)) +R (1st ‘(2nd𝑥)))
3017, 20cfv 6348 . . . . . . . 8 class (2nd ‘(1st𝑥))
3121, 20cfv 6348 . . . . . . . 8 class (2nd ‘(2nd𝑥))
3230, 31, 28co 7145 . . . . . . 7 class ((2nd ‘(1st𝑥)) +R (2nd ‘(2nd𝑥)))
3329, 32cop 4563 . . . . . 6 class ⟨((1st ‘(1st𝑥)) +R (1st ‘(2nd𝑥))), ((2nd ‘(1st𝑥)) +R (2nd ‘(2nd𝑥)))⟩
3425, 33, 21cif 4463 . . . . 5 class if((2nd𝑥) ∈ ℂ, ⟨((1st ‘(1st𝑥)) +R (1st ‘(2nd𝑥))), ((2nd ‘(1st𝑥)) +R (2nd ‘(2nd𝑥)))⟩, (2nd𝑥))
3524, 34, 17cif 4463 . . . 4 class if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ⟨((1st ‘(1st𝑥)) +R (1st ‘(2nd𝑥))), ((2nd ‘(1st𝑥)) +R (2nd ‘(2nd𝑥)))⟩, (2nd𝑥)), (1st𝑥))
3623, 18, 35cif 4463 . . 3 class if(((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞), ∞, if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ⟨((1st ‘(1st𝑥)) +R (1st ‘(2nd𝑥))), ((2nd ‘(1st𝑥)) +R (2nd ‘(2nd𝑥)))⟩, (2nd𝑥)), (1st𝑥)))
372, 14, 36cmpt 5137 . 2 class (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ))) ↦ if(((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞), ∞, if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ⟨((1st ‘(1st𝑥)) +R (1st ‘(2nd𝑥))), ((2nd ‘(1st𝑥)) +R (2nd ‘(2nd𝑥)))⟩, (2nd𝑥)), (1st𝑥))))
381, 37wceq 1528 1 wff +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ))) ↦ if(((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞), ∞, if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ⟨((1st ‘(1st𝑥)) +R (1st ‘(2nd𝑥))), ((2nd ‘(1st𝑥)) +R (2nd ‘(2nd𝑥)))⟩, (2nd𝑥)), (1st𝑥))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator