Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Definition and basic properties
mpllvec
Next ⟩
mplcrng
Metamath Proof Explorer
Ascii
Unicode
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