Definition df-bj-invc 38262

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) ∉ ℂ̅. This definition relies on df-bj-mulc 38260, 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 38261	. 2 class ·-1
2		vx	. . 3 setvar 𝑥
3		cccbar 38229	. . . 4 class ℂ̅
4		ccchat 38246	. . . 4 class ℂ̂
5	3, 4	cun 4149	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1568	. . . . 5 class 𝑥
7		cc0 11203	. . . . 5 class 0
8	6, 7	wceq 1569	. . . 4 wff 𝑥 = 0
9		cinfty 38244	. . . 4 class ∞
10		cc 11201	. . . . . 6 class ℂ
11	6, 10	wcel 2144	. . . . 5 wff 𝑥 ∈ ℂ
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1568	. . . . . . . 8 class 𝑦
14		cmulc 38259	. . . . . . . 8 class ·ℂ̅
15	6, 13, 14	co 7420	. . . . . . 7 class (𝑥 ·ℂ̅ 𝑦)
16		c1 11204	. . . . . . 7 class 1
17	15, 16	wceq 1569	. . . . . 6 wff (𝑥 ·ℂ̅ 𝑦) = 1
18	17, 12, 10	crio 7376	. . . . 5 class (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1)
19	11, 18, 7	cif 4481	. . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)
20	8, 9, 19	cif 4481	. . 3 class if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0))
21	2, 5, 20	cmpt 5185	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)))
22	1, 21	wceq 1569	1 wff ·-1 = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)))

This definition is used by: (None)