Metamath Proof Explorer

Theorem ccfldextrr

Description: The field of the complex numbers is an extension of the field of the real numbers. (Contributed by Thierry Arnoux, 20-Jul-2023)

Ref Expression
Assertion ccfldextrr 
|- CCfld /FldExt RRfld

Proof

Step Hyp Ref Expression
1 df-refld 
 |-  RRfld = ( CCfld |`s RR )
2 rebase 
 |-  RR = ( Base ` RRfld )
3 2 oveq2i 
 |-  ( CCfld |`s RR ) = ( CCfld |`s ( Base ` RRfld ) )
4 1 3 eqtri 
 |-  RRfld = ( CCfld |`s ( Base ` RRfld ) )
5 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
6 5 simpli 
 |-  RR e. ( SubRing ` CCfld )
7 2 6 eqeltrri 
 |-  ( Base ` RRfld ) e. ( SubRing ` CCfld )
8 cndrng 
 |-  CCfld e. DivRing
9 cncrng 
 |-  CCfld e. CRing
10 isfld 
 |-  ( CCfld e. Field <-> ( CCfld e. DivRing /\ CCfld e. CRing ) )
11 8 9 10 mpbir2an 
 |-  CCfld e. Field
12 refld 
 |-  RRfld e. Field
13 brfldext 
 |-  ( ( CCfld e. Field /\ RRfld e. Field ) -> ( CCfld /FldExt RRfld <-> ( RRfld = ( CCfld |`s ( Base ` RRfld ) ) /\ ( Base ` RRfld ) e. ( SubRing ` CCfld ) ) ) )
14 11 12 13 mp2an 
 |-  ( CCfld /FldExt RRfld <-> ( RRfld = ( CCfld |`s ( Base ` RRfld ) ) /\ ( Base ` RRfld ) e. ( SubRing ` CCfld ) ) )
15 4 7 14 mpbir2an 
 |-  CCfld /FldExt RRfld