Metamath Proof Explorer

Theorem rerrext

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

Ref Expression
Assertion rerrext 
|- RRfld e. RRExt

Proof

Step Hyp Ref Expression
1 cnnrg 
 |-  CCfld e. NrmRing
2 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
3 2 simpli 
 |-  RR e. ( SubRing ` CCfld )
4 df-refld 
 |-  RRfld = ( CCfld |`s RR )
5 4 subrgnrg 
 |-  ( ( CCfld e. NrmRing /\ RR e. ( SubRing ` CCfld ) ) -> RRfld e. NrmRing )
6 1 3 5 mp2an 
 |-  RRfld e. NrmRing
7 2 simpri 
 |-  RRfld e. DivRing
8 6 7 pm3.2i 
 |-  ( RRfld e. NrmRing /\ RRfld e. DivRing )
9 rezh 
 |-  ( ZMod ` RRfld ) e. NrmMod
10 reofld 
 |-  RRfld e. oField
11 ofldchr 
 |-  ( RRfld e. oField -> ( chr ` RRfld ) = 0 )
12 10 11 ax-mp 
 |-  ( chr ` RRfld ) = 0
13 9 12 pm3.2i 
 |-  ( ( ZMod ` RRfld ) e. NrmMod /\ ( chr ` RRfld ) = 0 )
14 recusp 
 |-  RRfld e. CUnifSp
15 reust 
 |-  ( UnifSt ` RRfld ) = ( metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) )
16 14 15 pm3.2i 
 |-  ( RRfld e. CUnifSp /\ ( UnifSt ` RRfld ) = ( metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) ) )
17 rebase 
 |-  RR = ( Base ` RRfld )
18 eqid 
 |-  ( ( dist ` RRfld ) |` ( RR X. RR ) ) = ( ( dist ` RRfld ) |` ( RR X. RR ) )
19 eqid 
 |-  ( ZMod ` RRfld ) = ( ZMod ` RRfld )
20 17 18 19 isrrext 
 |-  ( RRfld e. RRExt <-> ( ( RRfld e. NrmRing /\ RRfld e. DivRing ) /\ ( ( ZMod ` RRfld ) e. NrmMod /\ ( chr ` RRfld ) = 0 ) /\ ( RRfld e. CUnifSp /\ ( UnifSt ` RRfld ) = ( metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) ) ) ) )
21 8 13 16 20 mpbir3an 
 |-  RRfld e. RRExt