Definition df-bj-invc 34534

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 (^-1_ℂ̅‘0) = ∞ 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 (^-1_ℂ̅‘0) ∉ ℂ̅. Note that this definition relies on df-bj-mulc 34532, which does not bypass ordinary complex multiplication, but defines extended complex multiplication on top of it. Therefore, we could have used directly / instead of (℩... ·_ℂ̅ ...). (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-bj-invc	⊢ -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-bj-invc

Step	Hyp	Ref	Expression
1		cinvc 34533	. 2 class -1ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 34501	. . . 4 class ℂ̅
4		ccchat 34518	. . . 4 class ℂ̂
5	3, 4	cun 3937	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1535	. . . . 5 class 𝑥
7		cc0 10540	. . . . 5 class 0
8	6, 7	wceq 1536	. . . 4 wff 𝑥 = 0
9		cinfty 34516	. . . 4 class ∞
10		cc 10538	. . . . . 6 class ℂ
11	6, 10	wcel 2113	. . . . 5 wff 𝑥 ∈ ℂ
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1535	. . . . . . . 8 class 𝑦
14		cmulc 34531	. . . . . . . 8 class ·ℂ̅
15	6, 13, 14	co 7159	. . . . . . 7 class (𝑥 ·ℂ̅ 𝑦)
16		c1 10541	. . . . . . 7 class 1
17	15, 16	wceq 1536	. . . . . 6 wff (𝑥 ·ℂ̅ 𝑦) = 1
18	17, 12, 10	crio 7116	. . . . 5 class (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1)
19	11, 18, 7	cif 4470	. . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)
20	8, 9, 19	cif 4470	. . 3 class if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0))
21	2, 5, 20	cmpt 5149	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)))
22	1, 21	wceq 1536	1 wff -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)))

This definition is referenced by: (None)