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 ) |