Metamath Proof Explorer

Theorem psr1cl

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

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

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 psr1cl.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 psr1cl.z 
 |-  .0. = ( 0g ` R )
6 psr1cl.o 
 |-  .1. = ( 1r ` R )
7 psr1cl.u 
 |-  U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )
8 psr1cl.b 
 |-  B = ( Base ` S )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 9 6 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
11 9 5 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
12 10 11 ifcld 
 |-  ( R e. Ring -> if ( x = ( I X. { 0 } ) , .1. , .0. ) e. ( Base ` R ) )
13 3 12 syl 
 |-  ( ph -> if ( x = ( I X. { 0 } ) , .1. , .0. ) e. ( Base ` R ) )
14 13 adantr 
 |-  ( ( ph /\ x e. D ) -> if ( x = ( I X. { 0 } ) , .1. , .0. ) e. ( Base ` R ) )
15 14 7 fmptd 
 |-  ( ph -> U : D --> ( Base ` R ) )
16 fvex 
 |-  ( Base ` R ) e. _V
17 ovex 
 |-  ( NN0 ^m I ) e. _V
18 4 17 rabex2 
 |-  D e. _V
19 16 18 elmap 
 |-  ( U e. ( ( Base ` R ) ^m D ) <-> U : D --> ( Base ` R ) )
20 15 19 sylibr 
 |-  ( ph -> U e. ( ( Base ` R ) ^m D ) )
21 1 9 4 8 2 psrbas 
 |-  ( ph -> B = ( ( Base ` R ) ^m D ) )
22 20 21 eleqtrrd 
 |-  ( ph -> U e. B )