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

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 |`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 )