Metamath Proof Explorer

Theorem cnrrext

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

Ref Expression
Assertion cnrrext ⊢ ℂ fld ∈ ℝExt

Proof

Step Hyp Ref Expression
1 cnnrg ⊢ ℂ fld ∈ NrmRing
2 cndrng ⊢ ℂ fld ∈ DivRing
3 1 2 pm3.2i ⊢ ℂ fld ∈ NrmRing ∧ ℂ fld ∈ DivRing
4 cnzh ⊢ ℤMod ⁡ ℂ fld ∈ NrmMod
5 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
6 5 fveq2i ⊢ chr ⁡ ℝ fld = chr ⁡ ℂ fld ↾ 𝑠 ℝ
7 reofld ⊢ ℝ fld ∈ oField
8 ofldchr ⊢ ℝ fld ∈ oField → chr ⁡ ℝ fld = 0
9 7 8 ax-mp ⊢ chr ⁡ ℝ fld = 0
10 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
11 10 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
12 subrgchr ⊢ ℝ ∈ SubRing ⁡ ℂ fld → chr ⁡ ℂ fld ↾ 𝑠 ℝ = chr ⁡ ℂ fld
13 11 12 ax-mp ⊢ chr ⁡ ℂ fld ↾ 𝑠 ℝ = chr ⁡ ℂ fld
14 6 9 13 3eqtr3ri ⊢ chr ⁡ ℂ fld = 0
15 4 14 pm3.2i ⊢ ℤMod ⁡ ℂ fld ∈ NrmMod ∧ chr ⁡ ℂ fld = 0
16 cnfldcusp ⊢ ℂ fld ∈ CUnifSp
17 eqid ⊢ UnifSt ⁡ ℂ fld = UnifSt ⁡ ℂ fld
18 17 cnflduss ⊢ UnifSt ⁡ ℂ fld = metUnif ⁡ abs ∘ −
19 16 18 pm3.2i ⊢ ℂ fld ∈ CUnifSp ∧ UnifSt ⁡ ℂ fld = metUnif ⁡ abs ∘ −
20 cnfldbas ⊢ ℂ = Base ℂ fld
21 cnmet ⊢ abs ∘ − ∈ Met ⁡ ℂ
22 metf ⊢ abs ∘ − ∈ Met ⁡ ℂ → abs ∘ − : ℂ × ℂ ⟶ ℝ
23 ffn ⊢ abs ∘ − : ℂ × ℂ ⟶ ℝ → abs ∘ − Fn ℂ × ℂ
24 21 22 23 mp2b ⊢ abs ∘ − Fn ℂ × ℂ
25 fnresdm ⊢ abs ∘ − Fn ℂ × ℂ → abs ∘ − ↾ ℂ × ℂ = abs ∘ −
26 24 25 ax-mp ⊢ abs ∘ − ↾ ℂ × ℂ = abs ∘ −
27 cnfldds ⊢ abs ∘ − = dist ⁡ ℂ fld
28 27 reseq1i ⊢ abs ∘ − ↾ ℂ × ℂ = dist ⁡ ℂ fld ↾ ℂ × ℂ
29 26 28 eqtr3i ⊢ abs ∘ − = dist ⁡ ℂ fld ↾ ℂ × ℂ
30 eqid ⊢ ℤMod ⁡ ℂ fld = ℤMod ⁡ ℂ fld
31 20 29 30 isrrext ⊢ ℂ fld ∈ ℝExt ↔ ℂ fld ∈ NrmRing ∧ ℂ fld ∈ DivRing ∧ ℤMod ⁡ ℂ fld ∈ NrmMod ∧ chr ⁡ ℂ fld = 0 ∧ ℂ fld ∈ CUnifSp ∧ UnifSt ⁡ ℂ fld = metUnif ⁡ abs ∘ −
32 3 15 19 31 mpbir3an ⊢ ℂ fld ∈ ℝExt