Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Additional definitions for (multivariate) polynomials
ismhp2
Next ⟩
ismhp3
Metamath Proof Explorer
Ascii
Unicode
Theorem
ismhp2
Description:
Deduce a homogeneous polynomial from its properties.
(Contributed by
SN
, 25-May-2024)
Ref
Expression
Hypotheses
ismhp.h
⊢
H
=
I
mHomP
R
ismhp.p
⊢
P
=
I
mPoly
R
ismhp.b
⊢
B
=
Base
P
ismhp.0
⊢
0
˙
=
0
R
ismhp.d
⊢
D
=
h
∈
ℕ
0
I
|
h
-1
ℕ
∈
Fin
ismhp.n
⊢
φ
→
N
∈
ℕ
0
ismhp2.1
⊢
φ
→
X
∈
B
ismhp2.2
⊢
φ
→
X
supp
0
˙
⊆
g
∈
D
|
∑
ℂ
fld
↾
𝑠
ℕ
0
g
=
N
Assertion
ismhp2
⊢
φ
→
X
∈
H
⁡
N
Proof
Step
Hyp
Ref
Expression
1
ismhp.h
⊢
H
=
I
mHomP
R
2
ismhp.p
⊢
P
=
I
mPoly
R
3
ismhp.b
⊢
B
=
Base
P
4
ismhp.0
⊢
0
˙
=
0
R
5
ismhp.d
⊢
D
=
h
∈
ℕ
0
I
|
h
-1
ℕ
∈
Fin
6
ismhp.n
⊢
φ
→
N
∈
ℕ
0
7
ismhp2.1
⊢
φ
→
X
∈
B
8
ismhp2.2
⊢
φ
→
X
supp
0
˙
⊆
g
∈
D
|
∑
ℂ
fld
↾
𝑠
ℕ
0
g
=
N
9
1
2
3
4
5
6
ismhp
⊢
φ
→
X
∈
H
⁡
N
↔
X
∈
B
∧
X
supp
0
˙
⊆
g
∈
D
|
∑
ℂ
fld
↾
𝑠
ℕ
0
g
=
N
10
7
8
9
mpbir2and
⊢
φ
→
X
∈
H
⁡
N