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 (invc ` 0 ) = infty 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 (invc ` 0 ) e/ CCbar. (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-bj-invc	|- invc = ( x e. (CCbar u. CChat ) |-> if ( x = 0 , infty , if ( x e. CC , ( 1 / x ) , 0 ) ) )

Detailed syntax breakdown of Definition df-bj-invc

Step	Hyp	Ref	Expression
1		cinvc 33134	. 2 class invc
2		vx	. . 3 setvar x
3		cccbar 33102	. . . 4 class CCbar
4		ccchat 33119	. . . 4 class CChat
5	3, 4	cun 3572	. . 3 class (CCbar u. CChat )
6	2	cv 1482	. . . . 5 class x
7		cc0 9936	. . . . 5 class 0
8	6, 7	wceq 1483	. . . 4 wff x = 0
9		cinfty 33117	. . . 4 class infty
10		cc 9934	. . . . . 6 class CC
11	6, 10	wcel 1990	. . . . 5 wff x e. CC
12		c1 9937	. . . . . 6 class 1
13		cdiv 10684	. . . . . 6 class /
14	12, 6, 13	co 6650	. . . . 5 class ( 1 / x )
15	11, 14, 7	cif 4086	. . . 4 class if ( x e. CC , ( 1 / x ) , 0 )
16	8, 9, 15	cif 4086	. . 3 class if ( x = 0 , infty , if ( x e. CC , ( 1 / x ) , 0 ) )
17	2, 5, 16	cmpt 4729	. 2 class ( x e. (CCbar u. CChat ) |-> if ( x = 0 , infty , if ( x e. CC , ( 1 / x ) , 0 ) ) )
18	1, 17	wceq 1483	1 wff invc = ( x e. (CCbar u. CChat ) |-> if ( x = 0 , infty , if ( x e. CC , ( 1 / x ) , 0 ) ) )

This definition is referenced by: (None)