Metamath Proof Explorer

Theorem fldextsralvec

Description: The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023)

Ref Expression
Assertion fldextsralvec 
|- ( E /FldExt F -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec )

Proof

Step Hyp Ref Expression
1 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
2 isfld 
 |-  ( E e. Field <-> ( E e. DivRing /\ E e. CRing ) )
3 1 2 sylib 
 |-  ( E /FldExt F -> ( E e. DivRing /\ E e. CRing ) )
4 3 simpld 
 |-  ( E /FldExt F -> E e. DivRing )
5 fldextress 
 |-  ( E /FldExt F -> F = ( E |`s ( Base ` F ) ) )
6 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
7 isfld 
 |-  ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
8 6 7 sylib 
 |-  ( E /FldExt F -> ( F e. DivRing /\ F e. CRing ) )
9 8 simpld 
 |-  ( E /FldExt F -> F e. DivRing )
10 5 9 eqeltrrd 
 |-  ( E /FldExt F -> ( E |`s ( Base ` F ) ) e. DivRing )
11 eqid 
 |-  ( Base ` F ) = ( Base ` F )
12 11 fldextsubrg 
 |-  ( E /FldExt F -> ( Base ` F ) e. ( SubRing ` E ) )
13 eqid 
 |-  ( ( subringAlg ` E ) ` ( Base ` F ) ) = ( ( subringAlg ` E ) ` ( Base ` F ) )
14 eqid 
 |-  ( E |`s ( Base ` F ) ) = ( E |`s ( Base ` F ) )
15 13 14 sralvec 
 |-  ( ( E e. DivRing /\ ( E |`s ( Base ` F ) ) e. DivRing /\ ( Base ` F ) e. ( SubRing ` E ) ) -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec )
16 4 10 12 15 syl3anc 
 |-  ( E /FldExt F -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec )