Metamath Proof Explorer

Theorem cnrrext

Description: The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018)

Ref Expression
Assertion cnrrext 
|- CCfld e. RRExt

Proof

Step Hyp Ref Expression
1 cnnrg 
 |-  CCfld e. NrmRing
2 cndrng 
 |-  CCfld e. DivRing
3 1 2 pm3.2i 
 |-  ( CCfld e. NrmRing /\ CCfld e. DivRing )
4 cnzh 
 |-  ( ZMod ` CCfld ) e. NrmMod
5 df-refld 
 |-  RRfld = ( CCfld |`s RR )
6 5 fveq2i 
 |-  ( chr ` RRfld ) = ( chr ` ( CCfld |`s RR ) )
7 reofld 
 |-  RRfld e. oField
8 ofldchr 
 |-  ( RRfld e. oField -> ( chr ` RRfld ) = 0 )
9 7 8 ax-mp 
 |-  ( chr ` RRfld ) = 0
10 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
11 10 simpli 
 |-  RR e. ( SubRing ` CCfld )
12 subrgchr 
 |-  ( RR e. ( SubRing ` CCfld ) -> ( chr ` ( CCfld |`s RR ) ) = ( chr ` CCfld ) )
13 11 12 ax-mp 
 |-  ( chr ` ( CCfld |`s RR ) ) = ( chr ` CCfld )
14 6 9 13 3eqtr3ri 
 |-  ( chr ` CCfld ) = 0
15 4 14 pm3.2i 
 |-  ( ( ZMod ` CCfld ) e. NrmMod /\ ( chr ` CCfld ) = 0 )
16 cnfldcusp 
 |-  CCfld e. CUnifSp
17 eqid 
 |-  ( UnifSt ` CCfld ) = ( UnifSt ` CCfld )
18 17 cnflduss 
 |-  ( UnifSt ` CCfld ) = ( metUnif ` ( abs o. - ) )
19 16 18 pm3.2i 
 |-  ( CCfld e. CUnifSp /\ ( UnifSt ` CCfld ) = ( metUnif ` ( abs o. - ) ) )
20 cnfldbas 
 |-  CC = ( Base ` CCfld )
21 cnmet 
 |-  ( abs o. - ) e. ( Met ` CC )
22 metf 
 |-  ( ( abs o. - ) e. ( Met ` CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
23 ffn 
 |-  ( ( abs o. - ) : ( CC X. CC ) --> RR -> ( abs o. - ) Fn ( CC X. CC ) )
24 21 22 23 mp2b 
 |-  ( abs o. - ) Fn ( CC X. CC )
25 fnresdm 
 |-  ( ( abs o. - ) Fn ( CC X. CC ) -> ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - ) )
26 24 25 ax-mp 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - )
27 cnfldds 
 |-  ( abs o. - ) = ( dist ` CCfld )
28 27 reseq1i 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )
29 26 28 eqtr3i 
 |-  ( abs o. - ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )
30 eqid 
 |-  ( ZMod ` CCfld ) = ( ZMod ` CCfld )
31 20 29 30 isrrext 
 |-  ( CCfld e. RRExt <-> ( ( CCfld e. NrmRing /\ CCfld e. DivRing ) /\ ( ( ZMod ` CCfld ) e. NrmMod /\ ( chr ` CCfld ) = 0 ) /\ ( CCfld e. CUnifSp /\ ( UnifSt ` CCfld ) = ( metUnif ` ( abs o. - ) ) ) ) )
32 3 15 19 31 mpbir3an 
 |-  CCfld e. RRExt