This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↾s ℝ )
2 rebase ⊢ ℝ = ( Base ‘ ℝfld )
3 2 oveq2i ⊢ ( ℂfld ↾s ℝ ) = ( ℂfld ↾s ( Base ‘ ℝfld ) )
4 1 3 eqtri ⊢ ℝfld = ( ℂfld ↾s ( 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 ↾s ( Base ‘ ℝfld ) ) ∧ ( Base ‘ ℝfld ) ∈ ( SubRing ‘ ℂfld ) ) ) )
14 11 12 13 mp2an ⊢ ( ℂfld /FldExt ℝfld ↔ ( ℝfld = ( ℂfld ↾s ( Base ‘ ℝfld ) ) ∧ ( Base ‘ ℝfld ) ∈ ( SubRing ‘ ℂfld ) ) )
15 4 7 14 mpbir2an ⊢ ℂfld /FldExt ℝfld