Metamath Proof Explorer

Theorem resscdrg

Description: The real numbers are a subset of any complete subfield in the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis resscdrg.1 
|- F = ( CCfld |`s K )
Assertion resscdrg 
|- ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> RR C_ K )

Proof

Step Hyp Ref Expression
1 resscdrg.1 
 |-  F = ( CCfld |`s K )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
4 ax-resscn 
 |-  RR C_ CC
5 qssre 
 |-  QQ C_ RR
6 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
7 2 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
8 6 7 restcls 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ RR C_ CC /\ QQ C_ RR ) -> ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = ( ( ( cls ` ( TopOpen ` CCfld ) ) ` QQ ) i^i RR ) )
9 3 4 5 8 mp3an 
 |-  ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = ( ( ( cls ` ( TopOpen ` CCfld ) ) ` QQ ) i^i RR )
10 qdensere 
 |-  ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR
11 9 10 eqtr3i 
 |-  ( ( ( cls ` ( TopOpen ` CCfld ) ) ` QQ ) i^i RR ) = RR
12 sseqin2 
 |-  ( RR C_ ( ( cls ` ( TopOpen ` CCfld ) ) ` QQ ) <-> ( ( ( cls ` ( TopOpen ` CCfld ) ) ` QQ ) i^i RR ) = RR )
13 11 12 mpbir 
 |-  RR C_ ( ( cls ` ( TopOpen ` CCfld ) ) ` QQ )
14 simp3 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> F e. CMetSp )
15 cncms 
 |-  CCfld e. CMetSp
16 cnfldbas 
 |-  CC = ( Base ` CCfld )
17 16 subrgss 
 |-  ( K e. ( SubRing ` CCfld ) -> K C_ CC )
18 17 3ad2ant1 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> K C_ CC )
19 1 16 2 cmsss 
 |-  ( ( CCfld e. CMetSp /\ K C_ CC ) -> ( F e. CMetSp <-> K e. ( Clsd ` ( TopOpen ` CCfld ) ) ) )
20 15 18 19 sylancr 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> ( F e. CMetSp <-> K e. ( Clsd ` ( TopOpen ` CCfld ) ) ) )
21 14 20 mpbid 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> K e. ( Clsd ` ( TopOpen ` CCfld ) ) )
22 1 eleq1i 
 |-  ( F e. DivRing <-> ( CCfld |`s K ) e. DivRing )
23 qsssubdrg 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ ( CCfld |`s K ) e. DivRing ) -> QQ C_ K )
24 22 23 sylan2b 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing ) -> QQ C_ K )
25 24 3adant3 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> QQ C_ K )
26 6 clsss2 
 |-  ( ( K e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ QQ C_ K ) -> ( ( cls ` ( TopOpen ` CCfld ) ) ` QQ ) C_ K )
27 21 25 26 syl2anc 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> ( ( cls ` ( TopOpen ` CCfld ) ) ` QQ ) C_ K )
28 13 27 sstrid 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> RR C_ K )