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