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 32098
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
StepHypRef Expression
1 caddcc 32097 . 2 class +ℂ̅
2 vx . . 3 setvar 𝑥
3 cc 9790 . . . . . 6 class
4 cccbar 32075 . . . . . 6 class ℂ̅
53, 4cxp 5026 . . . . 5 class (ℂ × ℂ̅)
64, 3cxp 5026 . . . . 5 class (ℂ̅ × ℂ)
75, 6cun 3537 . . . 4 class ((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ))
8 ccchat 32092 . . . . . 6 class ℂ̂
98, 8cxp 5026 . . . . 5 class (ℂ̂ × ℂ̂)
10 cccinfty 32071 . . . . . 6 class
11 cdiag2 32061 . . . . . 6 class Diag
1210, 11cfv 5790 . . . . 5 class (Diag‘ℂ)
139, 12cun 3537 . . . 4 class ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ))
147, 13cun 3537 . . 3 class (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ)))
152cv 1473 . . . . . . 7 class 𝑥
16 c1st 7034 . . . . . . 7 class 1st
1715, 16cfv 5790 . . . . . 6 class (1st𝑥)
18 cinfty 32090 . . . . . 6 class
1917, 18wceq 1474 . . . . 5 wff (1st𝑥) = ∞
20 c2nd 7035 . . . . . . 7 class 2nd
2115, 20cfv 5790 . . . . . 6 class (2nd𝑥)
2221, 18wceq 1474 . . . . 5 wff (2nd𝑥) = ∞
2319, 22wo 381 . . . 4 wff ((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞)
2417, 3wcel 1976 . . . . 5 wff (1st𝑥) ∈ ℂ
2521, 3wcel 1976 . . . . . 6 wff (2nd𝑥) ∈ ℂ
26 caddc 9795 . . . . . . 7 class +
2717, 21, 26co 6527 . . . . . 6 class ((1st𝑥) + (2nd𝑥))
2825, 27, 21cif 4035 . . . . 5 class if((2nd𝑥) ∈ ℂ, ((1st𝑥) + (2nd𝑥)), (2nd𝑥))
2924, 28, 17cif 4035 . . . 4 class if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ((1st𝑥) + (2nd𝑥)), (2nd𝑥)), (1st𝑥))
3023, 18, 29cif 4035 . . 3 class if(((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞), ∞, if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ((1st𝑥) + (2nd𝑥)), (2nd𝑥)), (1st𝑥)))
312, 14, 30cmpt 4637 . 2 class (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ))) ↦ if(((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞), ∞, if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ((1st𝑥) + (2nd𝑥)), (2nd𝑥)), (1st𝑥))))
321, 31wceq 1474 1 wff +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ))) ↦ if(((1st𝑥) = ∞ ∨ (2nd𝑥) = ∞), ∞, if((1st𝑥) ∈ ℂ, if((2nd𝑥) ∈ ℂ, ((1st𝑥) + (2nd𝑥)), (2nd𝑥)), (1st𝑥))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator