This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 )