Metamath Proof Explorer

Theorem psr0

Description: The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrgrp.s 
|- S = ( I mPwSer R )
psrgrp.i 
|- ( ph -> I e. V )
psrgrp.r 
|- ( ph -> R e. Grp )
psr0.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psr0.o 
|- O = ( 0g ` R )
psr0.z 
|- .0. = ( 0g ` S )
Assertion psr0 
|- ( ph -> .0. = ( D X. { O } ) )

Proof

Step Hyp Ref Expression
1 psrgrp.s 
 |-  S = ( I mPwSer R )
2 psrgrp.i 
 |-  ( ph -> I e. V )
3 psrgrp.r 
 |-  ( ph -> R e. Grp )
4 psr0.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 psr0.o 
 |-  O = ( 0g ` R )
6 psr0.z 
 |-  .0. = ( 0g ` S )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 eqid 
 |-  ( +g ` S ) = ( +g ` S )
9 1 2 3 4 5 7 psr0cl 
 |-  ( ph -> ( D X. { O } ) e. ( Base ` S ) )
10 1 2 3 4 5 7 8 9 psr0lid 
 |-  ( ph -> ( ( D X. { O } ) ( +g ` S ) ( D X. { O } ) ) = ( D X. { O } ) )
11 1 2 3 psrgrp 
 |-  ( ph -> S e. Grp )
12 7 8 6 grpid 
 |-  ( ( S e. Grp /\ ( D X. { O } ) e. ( Base ` S ) ) -> ( ( ( D X. { O } ) ( +g ` S ) ( D X. { O } ) ) = ( D X. { O } ) <-> .0. = ( D X. { O } ) ) )
13 11 9 12 syl2anc 
 |-  ( ph -> ( ( ( D X. { O } ) ( +g ` S ) ( D X. { O } ) ) = ( D X. { O } ) <-> .0. = ( D X. { O } ) ) )
14 10 13 mpbid 
 |-  ( ph -> .0. = ( D X. { O } ) )