Metamath Proof Explorer

Theorem psr1

Description: The identity element of the ring of power series. (Contributed by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses psrring.s 
|- S = ( I mPwSer R )
psrring.i 
|- ( ph -> I e. V )
psrring.r 
|- ( ph -> R e. Ring )
psr1.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psr1.z 
|- .0. = ( 0g ` R )
psr1.o 
|- .1. = ( 1r ` R )
psr1.u 
|- U = ( 1r ` S )
Assertion psr1 
|- ( ph -> U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) )

Proof

Step Hyp Ref Expression
1 psrring.s 
 |-  S = ( I mPwSer R )
2 psrring.i 
 |-  ( ph -> I e. V )
3 psrring.r 
 |-  ( ph -> R e. Ring )
4 psr1.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 psr1.z 
 |-  .0. = ( 0g ` R )
6 psr1.o 
 |-  .1. = ( 1r ` R )
7 psr1.u 
 |-  U = ( 1r ` S )
8 eqid 
 |-  ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )
9 eqid 
 |-  ( Base ` S ) = ( Base ` S )
10 1 2 3 4 5 6 8 9 psr1cl 
 |-  ( ph -> ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) e. ( Base ` S ) )
11 2 adantr 
 |-  ( ( ph /\ y e. ( Base ` S ) ) -> I e. V )
12 3 adantr 
 |-  ( ( ph /\ y e. ( Base ` S ) ) -> R e. Ring )
13 eqid 
 |-  ( .r ` S ) = ( .r ` S )
14 simpr 
 |-  ( ( ph /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) )
15 1 11 12 4 5 6 8 9 13 14 psrlidm 
 |-  ( ( ph /\ y e. ( Base ` S ) ) -> ( ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ( .r ` S ) y ) = y )
16 1 11 12 4 5 6 8 9 13 14 psrridm 
 |-  ( ( ph /\ y e. ( Base ` S ) ) -> ( y ( .r ` S ) ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ) = y )
17 15 16 jca 
 |-  ( ( ph /\ y e. ( Base ` S ) ) -> ( ( ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ) = y ) )
18 17 ralrimiva 
 |-  ( ph -> A. y e. ( Base ` S ) ( ( ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ) = y ) )
19 1 2 3 psrring 
 |-  ( ph -> S e. Ring )
20 9 13 7 isringid 
 |-  ( S e. Ring -> ( ( ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) e. ( Base ` S ) /\ A. y e. ( Base ` S ) ( ( ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ) = y ) ) <-> U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ) )
21 19 20 syl 
 |-  ( ph -> ( ( ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) e. ( Base ` S ) /\ A. y e. ( Base ` S ) ( ( ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ) = y ) ) <-> U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) ) )
22 10 18 21 mpbi2and 
 |-  ( ph -> U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) )