Theorem mpl0

Description: The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mpl0.p	|- P = ( I mPoly R )
	mpl0.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
	mpl0.o	|- O = ( 0g ` R )
	mpl0.z	|- .0. = ( 0g ` P )
	mpl0.i	|- ( ph -> I e. W )
	mpl0.r	|- ( ph -> R e. Grp )
Assertion	mpl0	|- ( ph -> .0. = ( D X. { O } ) )

Proof

Step	Hyp	Ref	Expression
1		mpl0.p	|- P = ( I mPoly R )
2		mpl0.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3		mpl0.o	|- O = ( 0g ` R )
4		mpl0.z	|- .0. = ( 0g ` P )
5		mpl0.i	|- ( ph -> I e. W )
6		mpl0.r	|- ( ph -> R e. Grp )
7		eqid	|- ( I mPwSer R ) = ( I mPwSer R )
8		eqid	|- ( Base ` P ) = ( Base ` P )
9	7 1 8 5 6	mplsubg	|- ( ph -> ( Base ` P ) e. ( SubGrp ` ( I mPwSer R ) ) )
10	1 7 8	mplval2	|- P = ( ( I mPwSer R ) |`s ( Base ` P ) )
11		eqid	|- ( 0g ` ( I mPwSer R ) ) = ( 0g ` ( I mPwSer R ) )
12	10 11	subg0	|- ( ( Base ` P ) e. ( SubGrp ` ( I mPwSer R ) ) -> ( 0g ` ( I mPwSer R ) ) = ( 0g ` P ) )
13	9 12	syl	|- ( ph -> ( 0g ` ( I mPwSer R ) ) = ( 0g ` P ) )
14	7 5 6 2 3 11	psr0	|- ( ph -> ( 0g ` ( I mPwSer R ) ) = ( D X. { O } ) )
15	13 14	eqtr3d	|- ( ph -> ( 0g ` P ) = ( D X. { O } ) )
16	4 15	eqtrid	|- ( ph -> .0. = ( D X. { O } ) )