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