This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psr0cl

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 )
psr0cl.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psr0cl.o 
|- .0. = ( 0g ` R )
psr0cl.b 
|- B = ( Base ` S )
Assertion psr0cl 
|- ( ph -> ( D X. { .0. } ) e. B )

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 psr0cl.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 psr0cl.o 
 |-  .0. = ( 0g ` R )
6 psr0cl.b 
 |-  B = ( Base ` S )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 7 5 grpidcl 
 |-  ( R e. Grp -> .0. e. ( Base ` R ) )
9 fconst6g 
 |-  ( .0. e. ( Base ` R ) -> ( D X. { .0. } ) : D --> ( Base ` R ) )
10 3 8 9 3syl 
 |-  ( ph -> ( D X. { .0. } ) : D --> ( Base ` R ) )
11 fvex 
 |-  ( Base ` R ) e. _V
12 ovex 
 |-  ( NN0 ^m I ) e. _V
13 4 12 rabex2 
 |-  D e. _V
14 11 13 elmap 
 |-  ( ( D X. { .0. } ) e. ( ( Base ` R ) ^m D ) <-> ( D X. { .0. } ) : D --> ( Base ` R ) )
15 10 14 sylibr 
 |-  ( ph -> ( D X. { .0. } ) e. ( ( Base ` R ) ^m D ) )
16 1 7 4 6 2 psrbas 
 |-  ( ph -> B = ( ( Base ` R ) ^m D ) )
17 15 16 eleqtrrd 
 |-  ( ph -> ( D X. { .0. } ) e. B )