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∈ℂ‾∪ℂ^⟼ifx=0∞ifx∈ℂιy∈ℂ|x⋅ℂ‾y=10

Detailed syntax breakdown

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