Metamath Proof Explorer

Definition df-bj-invc

Description: Define inversion, which maps a nonzero extended complex number or element of the complex projective line (Riemann sphere) to its inverse. Beware of the overloading: the equality ( invc0 ) = infty is to be understood in the complex projective line, but 0 as an extended complex number does not have an inverse, which we can state as ( invc0 ) e/ CCbar . Note that this definition relies on df-bj-mulc , which does not bypass ordinary complex multiplication, but defines extended complex multiplication on top of it. Therefore, we could have used directly / instead of ( iota_ ... .cc ... ) . (Contributed by BJ, 22-Jun-2019)

Ref Expression
Assertion df-bj-invc ⊢ ⋅ -1 = x ∈ ℂ ‾ ∪ ℂ ^ ⟼ if x = 0 ∞ if x ∈ ℂ ι y ∈ ℂ | x ⋅ ℂ ‾ y = 1 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinvc class ⋅ -1
1 vx setvar x
2 cccbar class ℂ ‾
3 ccchat class ℂ ^
4 2 3 cun class ℂ ‾ ∪ ℂ ^
5 1 cv setvar x
6 cc0 class 0
7 5 6 wceq wff x = 0
8 cinfty class ∞
9 cc class ℂ
10 5 9 wcel wff x ∈ ℂ
11 vy setvar y
12 cmulc class ⋅ ℂ ‾
13 11 cv setvar y
14 5 13 12 co class x ⋅ ℂ ‾ y
15 c1 class 1
16 14 15 wceq wff x ⋅ ℂ ‾ y = 1
17 16 11 9 crio class ι y ∈ ℂ | x ⋅ ℂ ‾ y = 1
18 10 17 6 cif class if x ∈ ℂ ι y ∈ ℂ | x ⋅ ℂ ‾ y = 1 0
19 7 8 18 cif class if x = 0 ∞ if x ∈ ℂ ι y ∈ ℂ | x ⋅ ℂ ‾ y = 1 0
20 1 4 19 cmpt class x ∈ ℂ ‾ ∪ ℂ ^ ⟼ if x = 0 ∞ if x ∈ ℂ ι y ∈ ℂ | x ⋅ ℂ ‾ y = 1 0
21 0 20 wceq wff ⋅ -1 = x ∈ ℂ ‾ ∪ ℂ ^ ⟼ if x = 0 ∞ if x ∈ ℂ ι y ∈ ℂ | x ⋅ ℂ ‾ y = 1 0