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=ImPolyR
Assertion mpllvec ⊢I∈V∧R∈DivRing→P∈LVec

Proof

Step Hyp Ref Expression
1 mplgrp.p ⊢P=ImPolyR
2 drngring ⊢R∈DivRing→R∈Ring
3 1 mpllmod ⊢I∈V∧R∈Ring→P∈LMod
4 2 3 sylan2 ⊢I∈V∧R∈DivRing→P∈LMod
5 simpl ⊢I∈V∧R∈DivRing→I∈V
6 simpr ⊢I∈V∧R∈DivRing→R∈DivRing
7 1 5 6 mplsca ⊢I∈V∧R∈DivRing→R=Scalar⁡P
8 7 6 eqeltrrd ⊢I∈V∧R∈DivRing→Scalar⁡P∈DivRing
9 eqid ⊢Scalar⁡P=Scalar⁡P
10 9 islvec ⊢P∈LVec↔P∈LMod∧Scalar⁡P∈DivRing
11 4 8 10 sylanbrc ⊢I∈V∧R∈DivRing→P∈LVec