Metamath Proof Explorer

Theorem mvrfval

Description: Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses mvrfval.v 
|- V = ( I mVar R )
mvrfval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
mvrfval.z 
|- .0. = ( 0g ` R )
mvrfval.o 
|- .1. = ( 1r ` R )
mvrfval.i 
|- ( ph -> I e. W )
mvrfval.r 
|- ( ph -> R e. Y )
Assertion mvrfval 
|- ( ph -> V = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) )

Proof

Step Hyp Ref Expression
1 mvrfval.v 
 |-  V = ( I mVar R )
2 mvrfval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
3 mvrfval.z 
 |-  .0. = ( 0g ` R )
4 mvrfval.o 
 |-  .1. = ( 1r ` R )
5 mvrfval.i 
 |-  ( ph -> I e. W )
6 mvrfval.r 
 |-  ( ph -> R e. Y )
7 5 elexd 
 |-  ( ph -> I e. _V )
8 6 elexd 
 |-  ( ph -> R e. _V )
9 5 mptexd 
 |-  ( ph -> ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) e. _V )
10 simpl 
 |-  ( ( i = I /\ r = R ) -> i = I )
11 10 oveq2d 
 |-  ( ( i = I /\ r = R ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
12 11 rabeqdv 
 |-  ( ( i = I /\ r = R ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
13 12 2 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
14 mpteq1 
 |-  ( i = I -> ( y e. i |-> if ( y = x , 1 , 0 ) ) = ( y e. I |-> if ( y = x , 1 , 0 ) ) )
15 14 adantr 
 |-  ( ( i = I /\ r = R ) -> ( y e. i |-> if ( y = x , 1 , 0 ) ) = ( y e. I |-> if ( y = x , 1 , 0 ) ) )
16 15 eqeq2d 
 |-  ( ( i = I /\ r = R ) -> ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) <-> f = ( y e. I |-> if ( y = x , 1 , 0 ) ) ) )
17 simpr 
 |-  ( ( i = I /\ r = R ) -> r = R )
18 17 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( 1r ` r ) = ( 1r ` R ) )
19 18 4 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( 1r ` r ) = .1. )
20 17 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( 0g ` r ) = ( 0g ` R ) )
21 20 3 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( 0g ` r ) = .0. )
22 16 19 21 ifbieq12d 
 |-  ( ( i = I /\ r = R ) -> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) = if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) )
23 13 22 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( 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 ) ) ) = ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) )
24 10 23 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( 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 ) ) ) ) = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) )
25 df-mvr 
 |-  mVar = ( i e. _V , r e. _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 ) ) ) ) )
26 24 25 ovmpoga 
 |-  ( ( I e. _V /\ R e. _V /\ ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) e. _V ) -> ( I mVar R ) = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) )
27 7 8 9 26 syl3anc 
 |-  ( ph -> ( I mVar R ) = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) )
28 1 27 syl5eq 
 |-  ( ph -> V = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) )