Metamath Proof Explorer

Theorem srafldlvec

Description: Given a subfield F of a field E , E may be considered as a vector space over F , which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023)

		Ref	Expression
	Hypotheses	sralvec.a	$⊢ A = subringAlg (E) (U)$
		sralvec.f	$⊢ F = E ↾_{𝑠} U$
	Assertion	srafldlvec	$⊢ (E \in Field \land F \in Field \land U \in SubRing (E)) \to A \in LVec$

Proof

Step	Hyp	Ref	Expression
1		sralvec.a	$⊢ A = subringAlg (E) (U)$
2		sralvec.f	$⊢ F = E ↾_{𝑠} U$
3		isfld	$⊢ E \in Field \leftrightarrow (E \in DivRing \land E \in CRing)$
4	3	simplbi	$⊢ E \in Field \to E \in DivRing$
5		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
6	5	simplbi	$⊢ F \in Field \to F \in DivRing$
7		id	$⊢ U \in SubRing (E) \to U \in SubRing (E)$
8	1 2	sralvec	$⊢ (E \in DivRing \land F \in DivRing \land U \in SubRing (E)) \to A \in LVec$
9	4 6 7 8	syl3an	$⊢ (E \in Field \land F \in Field \land U \in SubRing (E)) \to A \in LVec$