Metamath Proof Explorer

Theorem mpllvec

Description: The polynomial ring is a vector space. (Contributed by SN, 29-Feb-2024)

Ref Expression
Hypothesis mplgrp.p 
|- P = ( I mPoly R )
Assertion mpllvec 
|- ( ( I e. V /\ R e. DivRing ) -> P e. LVec )

Proof

Step Hyp Ref Expression
1 mplgrp.p 
 |-  P = ( I mPoly R )
2 drngring 
 |-  ( R e. DivRing -> R e. Ring )
3 1 mpllmod 
 |-  ( ( I e. V /\ R e. Ring ) -> P e. LMod )
4 2 3 sylan2 
 |-  ( ( I e. V /\ R e. DivRing ) -> P e. LMod )
5 simpl 
 |-  ( ( I e. V /\ R e. DivRing ) -> I e. V )
6 simpr 
 |-  ( ( I e. V /\ R e. DivRing ) -> R e. DivRing )
7 1 5 6 mplsca 
 |-  ( ( I e. V /\ R e. DivRing ) -> R = ( Scalar ` P ) )
8 7 6 eqeltrrd 
 |-  ( ( I e. V /\ R e. DivRing ) -> ( Scalar ` P ) e. DivRing )
9 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
10 9 islvec 
 |-  ( P e. LVec <-> ( P e. LMod /\ ( Scalar ` P ) e. DivRing ) )
11 4 8 10 sylanbrc 
 |-  ( ( I e. V /\ R e. DivRing ) -> P e. LVec )