Definition df-bj-invc 33135

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 33134	. 2 class -1ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 33102	. . . 4 class ℂ̅
4		ccchat 33119	. . . 4 class ℂ̂
5	3, 4	cun 3572	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1482	. . . . 5 class 𝑥
7		cc0 9936	. . . . 5 class 0
8	6, 7	wceq 1483	. . . 4 wff 𝑥 = 0
9		cinfty 33117	. . . 4 class ∞
10		cc 9934	. . . . . 6 class ℂ
11	6, 10	wcel 1990	. . . . 5 wff 𝑥 ∈ ℂ
12		c1 9937	. . . . . 6 class 1
13		cdiv 10684	. . . . . 6 class /
14	12, 6, 13	co 6650	. . . . 5 class (1 / 𝑥)
15	11, 14, 7	cif 4086	. . . 4 class if(𝑥 ∈ ℂ, (1 / 𝑥), 0)
16	8, 9, 15	cif 4086	. . 3 class if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (1 / 𝑥), 0))
17	2, 5, 16	cmpt 4729	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (1 / 𝑥), 0)))
18	1, 17	wceq 1483	1 wff -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (1 / 𝑥), 0)))

This definition is referenced by: (None)