This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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