Metamath Proof Explorer

Definition df-bj-addc

Description: Define the additions on the extended complex numbers (on the subset of ( CCbar X. CCbar ) where it makes sense) and on the complex projective line (Riemann sphere). We use the plural in "additions" since these are two different operations, even though +cc is overloaded. (Contributed by BJ, 22-Jun-2019)

Ref Expression
Assertion df-bj-addc 
|- +cc = ( x e. ( ( ( CC X. CCbar ) u. ( CCbar X. CC ) ) u. ( ( CChat X. CChat ) u. ( _I |` CCinfty ) ) ) |-> if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( ( 1st ` x ) e. CC , if ( ( 2nd ` x ) e. CC , <. ( ( 1st ` ( 1st ` x ) ) +R ( 1st ` ( 2nd ` x ) ) ) , ( ( 2nd ` ( 1st ` x ) ) +R ( 2nd ` ( 2nd ` x ) ) ) >. , ( 2nd ` x ) ) , ( 1st ` x ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 caddcc 
 |-  +cc
1 vx 
 |-  x
2 cc 
 |-  CC
3 cccbar 
 |-  CCbar
4 2 3 cxp 
 |-  ( CC X. CCbar )
5 3 2 cxp 
 |-  ( CCbar X. CC )
6 4 5 cun 
 |-  ( ( CC X. CCbar ) u. ( CCbar X. CC ) )
7 ccchat 
 |-  CChat
8 7 7 cxp 
 |-  ( CChat X. CChat )
9 cid 
 |-  _I
10 cccinfty 
 |-  CCinfty
11 9 10 cres 
 |-  ( _I |` CCinfty )
12 8 11 cun 
 |-  ( ( CChat X. CChat ) u. ( _I |` CCinfty ) )
13 6 12 cun 
 |-  ( ( ( CC X. CCbar ) u. ( CCbar X. CC ) ) u. ( ( CChat X. CChat ) u. ( _I |` CCinfty ) ) )
14 c1st 
 |-  1st
15 1 cv 
 |-  x
16 15 14 cfv 
 |-  ( 1st ` x )
17 cinfty 
 |-  infty
18 16 17 wceq 
 |-  ( 1st ` x ) = infty
19 c2nd 
 |-  2nd
20 15 19 cfv 
 |-  ( 2nd ` x )
21 20 17 wceq 
 |-  ( 2nd ` x ) = infty
22 18 21 wo 
 |-  ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty )
23 16 2 wcel 
 |-  ( 1st ` x ) e. CC
24 20 2 wcel 
 |-  ( 2nd ` x ) e. CC
25 16 14 cfv 
 |-  ( 1st ` ( 1st ` x ) )
26 cplr 
 |-  +R
27 20 14 cfv 
 |-  ( 1st ` ( 2nd ` x ) )
28 25 27 26 co 
 |-  ( ( 1st ` ( 1st ` x ) ) +R ( 1st ` ( 2nd ` x ) ) )
29 16 19 cfv 
 |-  ( 2nd ` ( 1st ` x ) )
30 20 19 cfv 
 |-  ( 2nd ` ( 2nd ` x ) )
31 29 30 26 co 
 |-  ( ( 2nd ` ( 1st ` x ) ) +R ( 2nd ` ( 2nd ` x ) ) )
32 28 31 cop 
 |-  <. ( ( 1st ` ( 1st ` x ) ) +R ( 1st ` ( 2nd ` x ) ) ) , ( ( 2nd ` ( 1st ` x ) ) +R ( 2nd ` ( 2nd ` x ) ) ) >.
33 24 32 20 cif 
 |-  if ( ( 2nd ` x ) e. CC , <. ( ( 1st ` ( 1st ` x ) ) +R ( 1st ` ( 2nd ` x ) ) ) , ( ( 2nd ` ( 1st ` x ) ) +R ( 2nd ` ( 2nd ` x ) ) ) >. , ( 2nd ` x ) )
34 23 33 16 cif 
 |-  if ( ( 1st ` x ) e. CC , if ( ( 2nd ` x ) e. CC , <. ( ( 1st ` ( 1st ` x ) ) +R ( 1st ` ( 2nd ` x ) ) ) , ( ( 2nd ` ( 1st ` x ) ) +R ( 2nd ` ( 2nd ` x ) ) ) >. , ( 2nd ` x ) ) , ( 1st ` x ) )
35 22 17 34 cif 
 |-  if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( ( 1st ` x ) e. CC , if ( ( 2nd ` x ) e. CC , <. ( ( 1st ` ( 1st ` x ) ) +R ( 1st ` ( 2nd ` x ) ) ) , ( ( 2nd ` ( 1st ` x ) ) +R ( 2nd ` ( 2nd ` x ) ) ) >. , ( 2nd ` x ) ) , ( 1st ` x ) ) )
36 1 13 35 cmpt 
 |-  ( x e. ( ( ( CC X. CCbar ) u. ( CCbar X. CC ) ) u. ( ( CChat X. CChat ) u. ( _I |` CCinfty ) ) ) |-> if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( ( 1st ` x ) e. CC , if ( ( 2nd ` x ) e. CC , <. ( ( 1st ` ( 1st ` x ) ) +R ( 1st ` ( 2nd ` x ) ) ) , ( ( 2nd ` ( 1st ` x ) ) +R ( 2nd ` ( 2nd ` x ) ) ) >. , ( 2nd ` x ) ) , ( 1st ` x ) ) ) )
37 0 36 wceq 
 |-  +cc = ( x e. ( ( ( CC X. CCbar ) u. ( CCbar X. CC ) ) u. ( ( CChat X. CChat ) u. ( _I |` CCinfty ) ) ) |-> if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( ( 1st ` x ) e. CC , if ( ( 2nd ` x ) e. CC , <. ( ( 1st ` ( 1st ` x ) ) +R ( 1st ` ( 2nd ` x ) ) ) , ( ( 2nd ` ( 1st ` x ) ) +R ( 2nd ` ( 2nd ` x ) ) ) >. , ( 2nd ` x ) ) , ( 1st ` x ) ) ) )