Theorem sralvec

Description: Given a sub division ring F of a division ring 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	sralvec	|- ( ( E e. DivRing /\ F e. DivRing /\ 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		eqid	|- ( ( subringAlg ` E ) ` U ) = ( ( subringAlg ` E ) ` U )
4	3	sralmod	|- ( U e. ( SubRing ` E ) -> ( ( subringAlg ` E ) ` U ) e. LMod )
5	4	3ad2ant3	|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> ( ( subringAlg ` E ) ` U ) e. LMod )
6	1 5	eqeltrid	|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> A e. LMod )
7	1	a1i	|- ( U e. ( SubRing ` E ) -> A = ( ( subringAlg ` E ) ` U ) )
8		eqid	|- ( Base ` E ) = ( Base ` E )
9	8	subrgss	|- ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) )
10	7 9	srasca	|- ( U e. ( SubRing ` E ) -> ( E |`s U ) = ( Scalar ` A ) )
11	2 10	syl5eq	|- ( U e. ( SubRing ` E ) -> F = ( Scalar ` A ) )
12	11	3ad2ant3	|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> F = ( Scalar ` A ) )
13		simp2	|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> F e. DivRing )
14	12 13	eqeltrrd	|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> ( Scalar ` A ) e. DivRing )
15		eqid	|- ( Scalar ` A ) = ( Scalar ` A )
16	15	islvec	|- ( A e. LVec <-> ( A e. LMod /\ ( Scalar ` A ) e. DivRing ) )
17	6 14 16	sylanbrc	|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> A e. LVec )