Metamath Proof Explorer

Theorem cnfldcj

Description: The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Revised by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion cnfldcj 
|- * = ( *r ` CCfld )

Proof

Step Hyp Ref Expression
1 cjf 
 |-  * : CC --> CC
2 cnex 
 |-  CC e. _V
3 fex2 
 |-  ( ( * : CC --> CC /\ CC e. _V /\ CC e. _V ) -> * e. _V )
4 1 2 2 3 mp3an 
 |-  * e. _V
5 cnfldstr 
 |-  CCfld Struct <. 1 , ; 1 3 >.
6 starvid 
 |-  *r = Slot ( *r ` ndx )
7 ssun2 
 |-  { <. ( *r ` ndx ) , * >. } C_ ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )
8 ssun1 
 |-  ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) C_ ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
9 df-cnfld 
 |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
10 8 9 sseqtrri 
 |-  ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) C_ CCfld
11 7 10 sstri 
 |-  { <. ( *r ` ndx ) , * >. } C_ CCfld
12 5 6 11 strfv 
 |-  ( * e. _V -> * = ( *r ` CCfld ) )
13 4 12 ax-mp 
 |-  * = ( *r ` CCfld )