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 ∈ V ∧ R ∈ DivRing → P ∈ LVec

Proof

Step Hyp Ref Expression
1 mplgrp.p ⊢ P = I mPoly R
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