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 e. _V , r e. _V \|-> ( n e. NN0 \|-> { f e. ( Base ` ( i mPoly r ) ) \| ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) \| ( `' h " NN ) e. Fin } \| ( ( CCfld \|`s NN0 ) gsum g ) = n } } ) )
2	1	reldmmpo	\|- Rel dom mHomP

Step

Hyp

Ref

Expression

df-mhp

 |-  mHomP = ( i e. _V , r e. _V |-> ( n e. NN0 |-> { f e. ( Base ` ( i mPoly r ) ) | ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )

reldmmpo

 |-  Rel dom mHomP