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 = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
2	1	reldmmpo	⊢ Rel dom mHomP