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 = ℂ fld ↾ 𝑠 K
Assertion resscdrg ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing ∧ F ∈ CMetSp → ℝ ⊆ K

Proof

Step Hyp Ref Expression
1 resscdrg.1 ⊢ F = ℂ fld ↾ 𝑠 K
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 ↾ 𝑡 ℝ
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 ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing ∧ F ∈ CMetSp → F ∈ CMetSp
15 cncms ⊢ ℂ fld ∈ CMetSp
16 cnfldbas ⊢ ℂ = Base ℂ fld
17 16 subrgss ⊢ K ∈ SubRing ⁡ ℂ fld → K ⊆ ℂ
18 17 3ad2ant1 ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing ∧ F ∈ CMetSp → K ⊆ ℂ
19 1 16 2 cmsss ⊢ ℂ fld ∈ CMetSp ∧ K ⊆ ℂ → F ∈ CMetSp ↔ K ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
20 15 18 19 sylancr ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing ∧ F ∈ CMetSp → F ∈ CMetSp ↔ K ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
21 14 20 mpbid ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing ∧ F ∈ CMetSp → K ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
22 1 eleq1i ⊢ F ∈ DivRing ↔ ℂ fld ↾ 𝑠 K ∈ DivRing
23 qsssubdrg ⊢ K ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 K ∈ DivRing → ℚ ⊆ K
24 22 23 sylan2b ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing → ℚ ⊆ K
25 24 3adant3 ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing ∧ F ∈ CMetSp → ℚ ⊆ K
26 6 clsss2 ⊢ K ∈ Clsd ⁡ TopOpen ⁡ ℂ fld ∧ ℚ ⊆ K → cls ⁡ TopOpen ⁡ ℂ fld ⁡ ℚ ⊆ K
27 21 25 26 syl2anc ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing ∧ F ∈ CMetSp → cls ⁡ TopOpen ⁡ ℂ fld ⁡ ℚ ⊆ K
28 13 27 sstrid ⊢ K ∈ SubRing ⁡ ℂ fld ∧ F ∈ DivRing ∧ F ∈ CMetSp → ℝ ⊆ K