Metamath Proof Explorer

Definition df-bj-oppc

Description: Define the negation (operation giving the opposite) on the set of extended complex numbers and the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019)

Ref Expression
Assertion df-bj-oppc 
|- -cc = ( x e. ( CCbar u. CChat ) |-> if ( x = infty , infty , if ( x e. CC , ( iota_ y e. CC ( x +cc y ) = 0 ) , ( inftyexpitau ` ( x +cc <. 1/2 , 0R >. ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 coppcc 
 |-  -cc
1 vx 
 |-  x
2 cccbar 
 |-  CCbar
3 ccchat 
 |-  CChat
4 2 3 cun 
 |-  ( CCbar u. CChat )
5 1 cv 
 |-  x
6 cinfty 
 |-  infty
7 5 6 wceq 
 |-  x = infty
8 cc 
 |-  CC
9 5 8 wcel 
 |-  x e. CC
10 vy 
 |-  y
11 caddcc 
 |-  +cc
12 10 cv 
 |-  y
13 5 12 11 co 
 |-  ( x +cc y )
14 cc0 
 |-  0
15 13 14 wceq 
 |-  ( x +cc y ) = 0
16 15 10 8 crio 
 |-  ( iota_ y e. CC ( x +cc y ) = 0 )
17 cinftyexpitau 
 |-  inftyexpitau
18 chalf 
 |-  1/2
19 c0r 
 |-  0R
20 18 19 cop 
 |-  <. 1/2 , 0R >.
21 5 20 11 co 
 |-  ( x +cc <. 1/2 , 0R >. )
22 21 17 cfv 
 |-  ( inftyexpitau ` ( x +cc <. 1/2 , 0R >. ) )
23 9 16 22 cif 
 |-  if ( x e. CC , ( iota_ y e. CC ( x +cc y ) = 0 ) , ( inftyexpitau ` ( x +cc <. 1/2 , 0R >. ) ) )
24 7 6 23 cif 
 |-  if ( x = infty , infty , if ( x e. CC , ( iota_ y e. CC ( x +cc y ) = 0 ) , ( inftyexpitau ` ( x +cc <. 1/2 , 0R >. ) ) ) )
25 1 4 24 cmpt 
 |-  ( x e. ( CCbar u. CChat ) |-> if ( x = infty , infty , if ( x e. CC , ( iota_ y e. CC ( x +cc y ) = 0 ) , ( inftyexpitau ` ( x +cc <. 1/2 , 0R >. ) ) ) ) )
26 0 25 wceq 
 |-  -cc = ( x e. ( CCbar u. CChat ) |-> if ( x = infty , infty , if ( x e. CC , ( iota_ y e. CC ( x +cc y ) = 0 ) , ( inftyexpitau ` ( x +cc <. 1/2 , 0R >. ) ) ) ) )