Theorem reldmmhp

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

	Ref	Expression
Assertion	reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$

Proof

Step	Hyp	Ref	Expression
1		df-mhp	$$⊢\mathrm{mHomP}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}|f\mathrm{supp}{0}_r\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$