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 6 15 19	ismhp2	\|- ( ph -> ( D X. { .0. } ) e. ( H ` N ) )

Metamath Proof Explorer

Theorem mhp0cl

Proof