Definition df-bj-invc 38137

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 38135, 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 38136	. 2 class -1ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 38104	. . . 4 class ℂ̅
4		ccchat 38121	. . . 4 class ℂ̂
5	3, 4	cun 3897	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1569	. . . . 5 class 𝑥
7		cc0 11181	. . . . 5 class 0
8	6, 7	wceq 1570	. . . 4 wff 𝑥 = 0
9		cinfty 38119	. . . 4 class ∞
10		cc 11179	. . . . . 6 class ℂ
11	6, 10	wcel 2145	. . . . 5 wff 𝑥 ∈ ℂ
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1569	. . . . . . . 8 class 𝑦
14		cmulc 38134	. . . . . . . 8 class ·ℂ̅
15	6, 13, 14	co 7412	. . . . . . 7 class (𝑥 ·ℂ̅ 𝑦)
16		c1 11182	. . . . . . 7 class 1
17	15, 16	wceq 1570	. . . . . 6 wff (𝑥 ·ℂ̅ 𝑦) = 1
18	17, 12, 10	crio 7368	. . . . 5 class (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1)
19	11, 18, 7	cif 4482	. . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)
20	8, 9, 19	cif 4482	. . 3 class if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0))
21	2, 5, 20	cmpt 5186	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)))
22	1, 21	wceq 1570	1 wff -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)))

This definition is used by: (None)