Definition df-bj-invc 32312

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) ∉ ℂ̅. (Contributed by BJ, 22-Jun-2019.)

Assertion

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

Detailed syntax breakdown of Definition df-bj-invc

Step	Hyp	Ref	Expression
1		cinvc 32311	. 2 class -1ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 32279	. . . 4 class ℂ̅
4		ccchat 32296	. . . 4 class ℂ̂
5	3, 4	cun 3538	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1474	. . . . 5 class 𝑥
7		cc0 9815	. . . . 5 class 0
8	6, 7	wceq 1475	. . . 4 wff 𝑥 = 0
9		cinfty 32294	. . . 4 class ∞
10		cc 9813	. . . . . 6 class ℂ
11	6, 10	wcel 1977	. . . . 5 wff 𝑥 ∈ ℂ
12		c1 9816	. . . . . 6 class 1
13		cdiv 10563	. . . . . 6 class /
14	12, 6, 13	co 6549	. . . . 5 class (1 / 𝑥)
15	11, 14, 7	cif 4036	. . . 4 class if(𝑥 ∈ ℂ, (1 / 𝑥), 0)
16	8, 9, 15	cif 4036	. . 3 class if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (1 / 𝑥), 0))
17	2, 5, 16	cmpt 4643	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (1 / 𝑥), 0)))
18	1, 17	wceq 1475	1 wff -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (1 / 𝑥), 0)))

This definition is referenced by: (None)