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 ⊢ 𝐹 = ( ℂfld ↾s 𝐾 )
Assertion resscdrg ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp ) → ℝ ⊆ 𝐾 )

Proof

Step Hyp Ref Expression
1 resscdrg.1 ⊢ 𝐹 = ( ℂfld ↾s 𝐾 )
2 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3 2 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 qssre ⊢ ℚ ⊆ ℝ
6 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
7 2 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
8 6 7 restcls ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ℝ ⊆ ℂ ∧ ℚ ⊆ ℝ ) → ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ( ( ( cls ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℚ ) ∩ ℝ ) )
9 3 4 5 8 mp3an ⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ( ( ( cls ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℚ ) ∩ ℝ )
10 qdensere ⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ
11 9 10 eqtr3i ⊢ ( ( ( cls ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℚ ) ∩ ℝ ) = ℝ
12 sseqin2 ⊢ ( ℝ ⊆ ( ( cls ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℚ ) ↔ ( ( ( cls ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℚ ) ∩ ℝ ) = ℝ )
13 11 12 mpbir ⊢ ℝ ⊆ ( ( cls ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℚ )
14 simp3 ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp ) → 𝐹 ∈ CMetSp )
15 cncms ⊢ ℂfld ∈ CMetSp
16 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
17 16 subrgss ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ⊆ ℂ )
18 17 3ad2ant1 ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp ) → 𝐾 ⊆ ℂ )
19 1 16 2 cmsss ⊢ ( ( ℂfld ∈ CMetSp ∧ 𝐾 ⊆ ℂ ) → ( 𝐹 ∈ CMetSp ↔ 𝐾 ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) )
20 15 18 19 sylancr ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp ) → ( 𝐹 ∈ CMetSp ↔ 𝐾 ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) )
21 14 20 mpbid ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp ) → 𝐾 ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
22 1 eleq1i ⊢ ( 𝐹 ∈ DivRing ↔ ( ℂfld ↾s 𝐾 ) ∈ DivRing )
23 qsssubdrg ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐾 ) ∈ DivRing ) → ℚ ⊆ 𝐾 )
24 22 23 sylan2b ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ) → ℚ ⊆ 𝐾 )
25 24 3adant3 ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp ) → ℚ ⊆ 𝐾 )
26 6 clsss2 ⊢ ( ( 𝐾 ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ∧ ℚ ⊆ 𝐾 ) → ( ( cls ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℚ ) ⊆ 𝐾 )
27 21 25 26 syl2anc ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp ) → ( ( cls ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℚ ) ⊆ 𝐾 )
28 13 27 sstrid ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp ) → ℝ ⊆ 𝐾 )