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

Metamath Proof Explorer

Theorem mhprcl

Description: Reverse closure for homogeneous polynomials, use elfvov1 and elfvov2 with reldmmhp for the reverse closure of I and R . (Contributed by SN, 4-Aug-2025)

Ref Expression
Hypotheses mhprcl.h ⊢ H = I mHomP R
mhprcl.x ⊢ φ → X ∈ H ⁡ N
Assertion mhprcl ⊢ φ → N ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 mhprcl.h ⊢ H = I mHomP R
2 mhprcl.x ⊢ φ → X ∈ H ⁡ N
3 eqid ⊢ I mPoly R = I mPoly R
4 eqid ⊢ Base I mPoly R = Base I mPoly R
5 eqid ⊢ 0 R = 0 R
6 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
7 reldmmhp ⊢ Rel ⁡ dom ⁡ mHomP
8 7 1 2 elfvov1 ⊢ φ → I ∈ V
9 7 1 2 elfvov2 ⊢ φ → R ∈ V
10 1 3 4 5 6 8 9 mhpfval ⊢ φ → H = n ∈ ℕ 0 ⟼ f ∈ Base I mPoly R | f supp 0 R ⊆ g ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = n
11 10 fveq1d ⊢ φ → H ⁡ N = n ∈ ℕ 0 ⟼ f ∈ Base I mPoly R | f supp 0 R ⊆ g ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = n ⁡ N
12 2 11 eleqtrd ⊢ φ → X ∈ n ∈ ℕ 0 ⟼ f ∈ Base I mPoly R | f supp 0 R ⊆ g ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = n ⁡ N
13 eqid ⊢ n ∈ ℕ 0 ⟼ f ∈ Base I mPoly R | f supp 0 R ⊆ g ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = n = n ∈ ℕ 0 ⟼ f ∈ Base I mPoly R | f supp 0 R ⊆ g ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = n
14 13 mptrcl ⊢ X ∈ n ∈ ℕ 0 ⟼ f ∈ Base I mPoly R | f supp 0 R ⊆ g ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = n ⁡ N → N ∈ ℕ 0
15 12 14 syl ⊢ φ → N ∈ ℕ 0