Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Definition and basic properties
mpl0
Next ⟩
mpladd
Metamath Proof Explorer
Ascii
Unicode
Theorem
mpl0
Description:
The zero polynomial.
(Contributed by
Mario Carneiro
, 9-Jan-2015)
Ref
Expression
Hypotheses
mpl0.p
⊢
P
=
I
mPoly
R
mpl0.d
⊢
D
=
f
∈
ℕ
0
I
|
f
-1
ℕ
∈
Fin
mpl0.o
⊢
O
=
0
R
mpl0.z
⊢
0
˙
=
0
P
mpl0.i
⊢
φ
→
I
∈
W
mpl0.r
⊢
φ
→
R
∈
Grp
Assertion
mpl0
⊢
φ
→
0
˙
=
D
×
O
Proof
Step
Hyp
Ref
Expression
1
mpl0.p
⊢
P
=
I
mPoly
R
2
mpl0.d
⊢
D
=
f
∈
ℕ
0
I
|
f
-1
ℕ
∈
Fin
3
mpl0.o
⊢
O
=
0
R
4
mpl0.z
⊢
0
˙
=
0
P
5
mpl0.i
⊢
φ
→
I
∈
W
6
mpl0.r
⊢
φ
→
R
∈
Grp
7
eqid
⊢
I
mPwSer
R
=
I
mPwSer
R
8
eqid
⊢
Base
P
=
Base
P
9
7
1
8
5
6
mplsubg
⊢
φ
→
Base
P
∈
SubGrp
⁡
I
mPwSer
R
10
1
7
8
mplval2
⊢
P
=
I
mPwSer
R
↾
𝑠
Base
P
11
eqid
⊢
0
I
mPwSer
R
=
0
I
mPwSer
R
12
10
11
subg0
⊢
Base
P
∈
SubGrp
⁡
I
mPwSer
R
→
0
I
mPwSer
R
=
0
P
13
9
12
syl
⊢
φ
→
0
I
mPwSer
R
=
0
P
14
7
5
6
2
3
11
psr0
⊢
φ
→
0
I
mPwSer
R
=
D
×
O
15
13
14
eqtr3d
⊢
φ
→
0
P
=
D
×
O
16
4
15
syl5eq
⊢
φ
→
0
˙
=
D
×
O