fldextsubrg

Description: Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

		Ref	Expression
	Hypothesis	fldextsubrg.1	$⊢ U = {Base}_{F}$
	Assertion	fldextsubrg	$⊢ E /_{FldExt} F \to U \in SubRing (E)$

Step	Hyp	Ref	Expression
1		fldextsubrg.1	$⊢ U = {Base}_{F}$
2		fldextfld1	$⊢ E /_{FldExt} F \to E \in Field$
3		fldextfld2	$⊢ E /_{FldExt} F \to F \in Field$
4		brfldext	$⊢ (E \in Field \land F \in Field) \to (E /_{FldExt} F \leftrightarrow (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E)))$
5	2 3 4	syl2anc	$⊢ E /_{FldExt} F \to (E /_{FldExt} F \leftrightarrow (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E)))$
6	5	ibi	$⊢ E /_{FldExt} F \to (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E))$
7	6	simprd	$⊢ E /_{FldExt} F \to {Base}_{F} \in SubRing (E)$
8	1 7	eqeltrid	$⊢ E /_{FldExt} F \to U \in SubRing (E)$

Metamath Proof Explorer