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 ⊢ ℂ fld /FldExt ℝ fld

Proof

Step Hyp Ref Expression
1 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
2 rebase ⊢ ℝ = Base ℝ fld
3 2 oveq2i ⊢ ℂ fld ↾ 𝑠 ℝ = ℂ fld ↾ 𝑠 Base ℝ fld
4 1 3 eqtri ⊢ ℝ fld = ℂ fld ↾ 𝑠 Base ℝ fld
5 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
6 5 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
7 2 6 eqeltrri ⊢ Base ℝ fld ∈ SubRing ⁡ ℂ fld
8 cndrng ⊢ ℂ fld ∈ DivRing
9 cncrng ⊢ ℂ fld ∈ CRing
10 isfld ⊢ ℂ fld ∈ Field ↔ ℂ fld ∈ DivRing ∧ ℂ fld ∈ CRing
11 8 9 10 mpbir2an ⊢ ℂ fld ∈ Field
12 refld ⊢ ℝ fld ∈ Field
13 brfldext ⊢ ℂ fld ∈ Field ∧ ℝ fld ∈ Field → ℂ fld /FldExt ℝ fld ↔ ℝ fld = ℂ fld ↾ 𝑠 Base ℝ fld ∧ Base ℝ fld ∈ SubRing ⁡ ℂ fld
14 11 12 13 mp2an ⊢ ℂ fld /FldExt ℝ fld ↔ ℝ fld = ℂ fld ↾ 𝑠 Base ℝ fld ∧ Base ℝ fld ∈ SubRing ⁡ ℂ fld
15 4 7 14 mpbir2an ⊢ ℂ fld /FldExt ℝ fld