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 |`s U )
Assertion	srafldlvec	|- ( ( E e. Field /\ F e. Field /\ U e. ( SubRing ` E ) ) -> A e. LVec )

Proof

Step	Hyp	Ref	Expression
1		sralvec.a	|- A = ( ( subringAlg ` E ) ` U )
2		sralvec.f	|- F = ( E |`s U )
3		isfld	|- ( E e. Field <-> ( E e. DivRing /\ E e. CRing ) )
4	3	simplbi	|- ( E e. Field -> E e. DivRing )
5		isfld	|- ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
6	5	simplbi	|- ( F e. Field -> F e. DivRing )
7		id	|- ( U e. ( SubRing ` E ) -> U e. ( SubRing ` E ) )
8	1 2	sralvec	|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> A e. LVec )
9	4 6 7 8	syl3an	|- ( ( E e. Field /\ F e. Field /\ U e. ( SubRing ` E ) ) -> A e. LVec )