Metamath Proof Explorer

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 syl5eq 
 |-  ( ph -> .0. = ( D X. { O } ) )