Metamath Proof Explorer


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