Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Definition and basic properties
mpllmod
Next ⟩
mplring
Metamath Proof Explorer
Ascii
Unicode
Theorem
mpllmod
Description:
The polynomial ring is a left module.
(Contributed by
Mario Carneiro
, 9-Jan-2015)
Ref
Expression
Hypothesis
mplgrp.p
⊢
P
=
I
mPoly
R
Assertion
mpllmod
⊢
I
∈
V
∧
R
∈
Ring
→
P
∈
LMod
Proof
Step
Hyp
Ref
Expression
1
mplgrp.p
⊢
P
=
I
mPoly
R
2
eqid
⊢
I
mPwSer
R
=
I
mPwSer
R
3
simpl
⊢
I
∈
V
∧
R
∈
Ring
→
I
∈
V
4
simpr
⊢
I
∈
V
∧
R
∈
Ring
→
R
∈
Ring
5
2
3
4
psrlmod
⊢
I
∈
V
∧
R
∈
Ring
→
I
mPwSer
R
∈
LMod
6
eqid
⊢
Base
P
=
Base
P
7
2
1
6
3
4
mpllss
⊢
I
∈
V
∧
R
∈
Ring
→
Base
P
∈
LSubSp
⁡
I
mPwSer
R
8
1
2
6
mplval2
⊢
P
=
I
mPwSer
R
↾
𝑠
Base
P
9
eqid
⊢
LSubSp
⁡
I
mPwSer
R
=
LSubSp
⁡
I
mPwSer
R
10
8
9
lsslmod
⊢
I
mPwSer
R
∈
LMod
∧
Base
P
∈
LSubSp
⁡
I
mPwSer
R
→
P
∈
LMod
11
5
7
10
syl2anc
⊢
I
∈
V
∧
R
∈
Ring
→
P
∈
LMod