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

Metamath Proof Explorer

Theorem reldmmhp

Description: The domain of the homogeneous polynomial operator is a relation. (Contributed by SN, 18-May-2025)

Ref Expression
Assertion reldmmhp ⊢ Rel ⁡ dom ⁡ mHomP

Proof

Step Hyp Ref Expression
1 df-mhp ⊢ mHomP = i ∈ V , r ∈ V ⟼ n ∈ ℕ 0 ⟼ f ∈ Base i mPoly r | f supp 0 r ⊆ g ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = n
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ mHomP