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 )