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	$$⊢{ℂ}_{\mathrm{fld}}{/}_{\mathrm{FldExt}}{ℝ}_{\mathrm{fld}}$$

Proof

Step	Hyp	Ref	Expression
1		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
2		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
3	2	oveq2i	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
4	1 3	eqtri	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
5		resubdrg	$$⊢\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$$
6	5	simpli	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
7	2 6	eqeltrri	$$⊢{\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
8		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
9		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
10		isfld	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}\leftrightarrow \left({ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\right)$$
11	8 9 10	mpbir2an	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
12		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
13		brfldext	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Field}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{Field}\right)\to \left({ℂ}_{\mathrm{fld}}{/}_{\mathrm{FldExt}}{ℝ}_{\mathrm{fld}}\leftrightarrow \left({ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}\wedge {\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)$$
14	11 12 13	mp2an	$$⊢{ℂ}_{\mathrm{fld}}{/}_{\mathrm{FldExt}}{ℝ}_{\mathrm{fld}}\leftrightarrow \left({ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}\wedge {\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
15	4 7 14	mpbir2an	$$⊢{ℂ}_{\mathrm{fld}}{/}_{\mathrm{FldExt}}{ℝ}_{\mathrm{fld}}$$