fldextsralvec

Description: The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023)

		Ref	Expression
	Assertion	fldextsralvec	$⊢ E /_{FldExt} F \to subringAlg (E) ({Base}_{F}) \in LVec$

Step	Hyp	Ref	Expression
1		fldextfld1	$⊢ E /_{FldExt} F \to E \in Field$
2		isfld	$⊢ E \in Field \leftrightarrow (E \in DivRing \land E \in CRing)$
3	1 2	sylib	$⊢ E /_{FldExt} F \to (E \in DivRing \land E \in CRing)$
4	3	simpld	$⊢ E /_{FldExt} F \to E \in DivRing$
5		fldextress	$⊢ E /_{FldExt} F \to F = E ↾_{𝑠} {Base}_{F}$
6		fldextfld2	$⊢ E /_{FldExt} F \to F \in Field$
7		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
8	6 7	sylib	$⊢ E /_{FldExt} F \to (F \in DivRing \land F \in CRing)$
9	8	simpld	$⊢ E /_{FldExt} F \to F \in DivRing$
10	5 9	eqeltrrd	$⊢ E /_{FldExt} F \to E ↾_{𝑠} {Base}_{F} \in DivRing$
11		eqid	$⊢ {Base}_{F} = {Base}_{F}$
12	11	fldextsubrg	$⊢ E /_{FldExt} F \to {Base}_{F} \in SubRing (E)$
13		eqid	$⊢ subringAlg (E) ({Base}_{F}) = subringAlg (E) ({Base}_{F})$
14		eqid	$⊢ E ↾_{𝑠} {Base}_{F} = E ↾_{𝑠} {Base}_{F}$
15	13 14	sralvec	$⊢ (E \in DivRing \land E ↾_{𝑠} {Base}_{F} \in DivRing \land {Base}_{F} \in SubRing (E)) \to subringAlg (E) ({Base}_{F}) \in LVec$
16	4 10 12 15	syl3anc	$⊢ E /_{FldExt} F \to subringAlg (E) ({Base}_{F}) \in LVec$

Metamath Proof Explorer