Theorem mhp0cl

Description: The zero polynomial is homogeneous. Under df-mhp , it has any (nonnegative integer) degree which loosely corresponds to the value "undefined". The values -oo and 0 are also used in Metamath (by df-mdeg and df-dgr respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 . (Contributed by SN, 12-Sep-2023)

	Ref	Expression
Hypotheses	mhp0cl.h	|- H = ( I mHomP R )
	mhp0cl.0	|- .0. = ( 0g ` R )
	mhp0cl.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	mhp0cl.i	|- ( ph -> I e. V )
	mhp0cl.r	|- ( ph -> R e. Grp )
	mhp0cl.n	|- ( ph -> N e. NN0 )
Assertion	mhp0cl	|- ( ph -> ( D X. { .0. } ) e. ( H ` N ) )

Proof

Step	Hyp	Ref	Expression
1		mhp0cl.h	|- H = ( I mHomP R )
2		mhp0cl.0	|- .0. = ( 0g ` R )
3		mhp0cl.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
4		mhp0cl.i	|- ( ph -> I e. V )
5		mhp0cl.r	|- ( ph -> R e. Grp )
6		mhp0cl.n	|- ( ph -> N e. NN0 )
7		eqid	|- ( I mPoly R ) = ( I mPoly R )
8		eqid	|- ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
9		eqid	|- ( 0g ` ( I mPoly R ) ) = ( 0g ` ( I mPoly R ) )
10	7 3 2 9 4 5	mpl0	|- ( ph -> ( 0g ` ( I mPoly R ) ) = ( D X. { .0. } ) )
11	7	mplgrp	|- ( ( I e. V /\ R e. Grp ) -> ( I mPoly R ) e. Grp )
12	4 5 11	syl2anc	|- ( ph -> ( I mPoly R ) e. Grp )
13	8 9	grpidcl	|- ( ( I mPoly R ) e. Grp -> ( 0g ` ( I mPoly R ) ) e. ( Base ` ( I mPoly R ) ) )
14	12 13	syl	|- ( ph -> ( 0g ` ( I mPoly R ) ) e. ( Base ` ( I mPoly R ) ) )
15	10 14	eqeltrrd	|- ( ph -> ( D X. { .0. } ) e. ( Base ` ( I mPoly R ) ) )
16		fczsupp0	|- ( ( D X. { .0. } ) supp .0. ) = (/)
17		0ss	|- (/) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N }
18	16 17	eqsstri	|- ( ( D X. { .0. } ) supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N }
19	18	a1i	|- ( ph -> ( ( D X. { .0. } ) supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
20	1 7 8 2 3 4 5 6 15 19	ismhp2	|- ( ph -> ( D X. { .0. } ) e. ( H ` N ) )