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

Metamath Proof Explorer

Theorem psr0lid

Description: The zero element of the ring of power series is a left identity. (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 )
psr0lid.p 
|- .+ = ( +g ` S )
psr0lid.x 
|- ( ph -> X e. B )
Assertion psr0lid 
|- ( ph -> ( ( D X. { .0. } ) .+ X ) = X )

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 psr0lid.p 
 |-  .+ = ( +g ` S )
8 psr0lid.x 
 |-  ( ph -> X e. B )
9 eqid 
 |-  ( +g ` R ) = ( +g ` R )
10 1 2 3 4 5 6 psr0cl 
 |-  ( ph -> ( D X. { .0. } ) e. B )
11 1 6 9 7 10 8 psradd 
 |-  ( ph -> ( ( D X. { .0. } ) .+ X ) = ( ( D X. { .0. } ) oF ( +g ` R ) X ) )
12 ovex 
 |-  ( NN0 ^m I ) e. _V
13 4 12 rabex2 
 |-  D e. _V
14 13 a1i 
 |-  ( ph -> D e. _V )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 1 15 4 6 8 psrelbas 
 |-  ( ph -> X : D --> ( Base ` R ) )
17 5 fvexi 
 |-  .0. e. _V
18 17 a1i 
 |-  ( ph -> .0. e. _V )
19 15 9 5 grplid 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( .0. ( +g ` R ) x ) = x )
20 3 19 sylan 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( .0. ( +g ` R ) x ) = x )
21 14 16 18 20 caofid0l 
 |-  ( ph -> ( ( D X. { .0. } ) oF ( +g ` R ) X ) = X )
22 11 21 eqtrd 
 |-  ( ph -> ( ( D X. { .0. } ) .+ X ) = X )