Metamath Proof Explorer

Theorem mvrf

Description: The power series variable function is a function from the index set to elements of the power series structure representing X i for each i . (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses mvrf.s 
|- S = ( I mPwSer R )
mvrf.v 
|- V = ( I mVar R )
mvrf.b 
|- B = ( Base ` S )
mvrf.i 
|- ( ph -> I e. W )
mvrf.r 
|- ( ph -> R e. Ring )
Assertion mvrf 
|- ( ph -> V : I --> B )

Proof

Step Hyp Ref Expression
1 mvrf.s 
 |-  S = ( I mPwSer R )
2 mvrf.v 
 |-  V = ( I mVar R )
3 mvrf.b 
 |-  B = ( Base ` S )
4 mvrf.i 
 |-  ( ph -> I e. W )
5 mvrf.r 
 |-  ( ph -> R e. Ring )
6 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 2 6 7 8 4 5 mvrfval 
 |-  ( ph -> V = ( x e. I |-> ( f e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 10 8 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
12 5 11 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
13 10 7 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
14 5 13 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
15 12 14 ifcld 
 |-  ( ph -> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
16 15 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ f e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
17 16 fmpttd 
 |-  ( ( ph /\ x e. I ) -> ( f e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
18 fvex 
 |-  ( Base ` R ) e. _V
19 ovex 
 |-  ( NN0 ^m I ) e. _V
20 19 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
21 18 20 elmap 
 |-  ( ( f e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) <-> ( f e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
22 17 21 sylibr 
 |-  ( ( ph /\ x e. I ) -> ( f e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
23 1 10 6 3 4 psrbas 
 |-  ( ph -> B = ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
24 23 adantr 
 |-  ( ( ph /\ x e. I ) -> B = ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
25 22 24 eleqtrrd 
 |-  ( ( ph /\ x e. I ) -> ( f e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. B )
26 9 25 fmpt3d 
 |-  ( ph -> V : I --> B )