Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Additional definitions for (multivariate) polynomials
mhpmpl
Next ⟩
mhpdeg
Metamath Proof Explorer
Ascii
Unicode
Theorem
mhpmpl
Description:
A homogeneous polynomial is a polynomial.
(Contributed by
Steven Nguyen
, 25-Aug-2023)
Ref
Expression
Hypotheses
mhpmpl.h
⊢
H
=
I
mHomP
R
mhpmpl.p
⊢
P
=
I
mPoly
R
mhpmpl.b
⊢
B
=
Base
P
mhpmpl.x
⊢
φ
→
X
∈
H
⁡
N
Assertion
mhpmpl
⊢
φ
→
X
∈
B
Proof
Step
Hyp
Ref
Expression
1
mhpmpl.h
⊢
H
=
I
mHomP
R
2
mhpmpl.p
⊢
P
=
I
mPoly
R
3
mhpmpl.b
⊢
B
=
Base
P
4
mhpmpl.x
⊢
φ
→
X
∈
H
⁡
N
5
eqid
⊢
0
R
=
0
R
6
eqid
⊢
h
∈
ℕ
0
I
|
h
-1
ℕ
∈
Fin
=
h
∈
ℕ
0
I
|
h
-1
ℕ
∈
Fin
7
1
4
mhprcl
⊢
φ
→
N
∈
ℕ
0
8
1
2
3
5
6
7
ismhp
⊢
φ
→
X
∈
H
⁡
N
↔
X
∈
B
∧
X
supp
0
R
⊆
g
∈
h
∈
ℕ
0
I
|
h
-1
ℕ
∈
Fin
|
∑
ℂ
fld
↾
𝑠
ℕ
0
g
=
N
9
8
simprbda
⊢
φ
∧
X
∈
H
⁡
N
→
X
∈
B
10
4
9
mpdan
⊢
φ
→
X
∈
B