Metamath Proof Explorer

Theorem mrsubffval

Description: The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubffval.c 
|- C = ( mCN ` T )
mrsubffval.v 
|- V = ( mVR ` T )
mrsubffval.r 
|- R = ( mREx ` T )
mrsubffval.s 
|- S = ( mRSubst ` T )
mrsubffval.g 
|- G = ( freeMnd ` ( C u. V ) )
Assertion mrsubffval 
|- ( T e. W -> S = ( f e. ( R ^pm V ) |-> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mrsubffval.c 
 |-  C = ( mCN ` T )
2 mrsubffval.v 
 |-  V = ( mVR ` T )
3 mrsubffval.r 
 |-  R = ( mREx ` T )
4 mrsubffval.s 
 |-  S = ( mRSubst ` T )
5 mrsubffval.g 
 |-  G = ( freeMnd ` ( C u. V ) )
6 elex 
 |-  ( T e. W -> T e. _V )
7 fveq2 
 |-  ( t = T -> ( mREx ` t ) = ( mREx ` T ) )
8 7 3 eqtr4di 
 |-  ( t = T -> ( mREx ` t ) = R )
9 fveq2 
 |-  ( t = T -> ( mVR ` t ) = ( mVR ` T ) )
10 9 2 eqtr4di 
 |-  ( t = T -> ( mVR ` t ) = V )
11 8 10 oveq12d 
 |-  ( t = T -> ( ( mREx ` t ) ^pm ( mVR ` t ) ) = ( R ^pm V ) )
12 fveq2 
 |-  ( t = T -> ( mCN ` t ) = ( mCN ` T ) )
13 12 1 eqtr4di 
 |-  ( t = T -> ( mCN ` t ) = C )
14 13 10 uneq12d 
 |-  ( t = T -> ( ( mCN ` t ) u. ( mVR ` t ) ) = ( C u. V ) )
15 14 fveq2d 
 |-  ( t = T -> ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) = ( freeMnd ` ( C u. V ) ) )
16 15 5 eqtr4di 
 |-  ( t = T -> ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) = G )
17 14 mpteq1d 
 |-  ( t = T -> ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) = ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) )
18 17 coeq1d 
 |-  ( t = T -> ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) = ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) )
19 16 18 oveq12d 
 |-  ( t = T -> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) = ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) )
20 8 19 mpteq12dv 
 |-  ( t = T -> ( e e. ( mREx ` t ) |-> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) )
21 11 20 mpteq12dv 
 |-  ( t = T -> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mREx ` t ) |-> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) = ( f e. ( R ^pm V ) |-> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )
22 df-mrsub 
 |-  mRSubst = ( t e. _V |-> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mREx ` t ) |-> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )
23 ovex 
 |-  ( R ^pm V ) e. _V
24 23 mptex 
 |-  ( f e. ( R ^pm V ) |-> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) e. _V
25 21 22 24 fvmpt 
 |-  ( T e. _V -> ( mRSubst ` T ) = ( f e. ( R ^pm V ) |-> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )
26 6 25 syl 
 |-  ( T e. W -> ( mRSubst ` T ) = ( f e. ( R ^pm V ) |-> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )
27 4 26 syl5eq 
 |-  ( T e. W -> S = ( f e. ( R ^pm V ) |-> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )