Metamath Proof Explorer

Theorem mrsubfval

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 mrsubfval 
|- ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( 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 1 2 3 4 5 mrsubffval 
 |-  ( T e. _V -> 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 ) ) ) ) )
7 6 adantr 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> 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 ) ) ) ) )
8 dmeq 
 |-  ( f = F -> dom f = dom F )
9 fdm 
 |-  ( F : A --> R -> dom F = A )
10 9 ad2antrl 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> dom F = A )
11 8 10 sylan9eqr 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> dom f = A )
12 11 eleq2d 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> ( v e. dom f <-> v e. A ) )
13 simpr 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> f = F )
14 13 fveq1d 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> ( f ` v ) = ( F ` v ) )
15 12 14 ifbieq1d 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> if ( v e. dom f , ( f ` v ) , <" v "> ) = if ( v e. A , ( F ` v ) , <" v "> ) )
16 15 mpteq2dv 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) = ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) )
17 16 coeq1d 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) = ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) )
18 17 oveq2d 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) = ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) )
19 18 mpteq2dv 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) )
20 3 fvexi 
 |-  R e. _V
21 20 a1i 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> R e. _V )
22 2 fvexi 
 |-  V e. _V
23 22 a1i 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> V e. _V )
24 simprl 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> F : A --> R )
25 simprr 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> A C_ V )
26 elpm2r 
 |-  ( ( ( R e. _V /\ V e. _V ) /\ ( F : A --> R /\ A C_ V ) ) -> F e. ( R ^pm V ) )
27 21 23 24 25 26 syl22anc 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> F e. ( R ^pm V ) )
28 20 mptex 
 |-  ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) e. _V
29 28 a1i 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) e. _V )
30 7 19 27 29 fvmptd 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> ( S ` F ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) )
31 30 ex 
 |-  ( T e. _V -> ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) ) )
32 0fv 
 |-  ( (/) ` F ) = (/)
33 fvprc 
 |-  ( -. T e. _V -> ( mRSubst ` T ) = (/) )
34 4 33 syl5eq 
 |-  ( -. T e. _V -> S = (/) )
35 34 fveq1d 
 |-  ( -. T e. _V -> ( S ` F ) = ( (/) ` F ) )
36 fvprc 
 |-  ( -. T e. _V -> ( mREx ` T ) = (/) )
37 3 36 syl5eq 
 |-  ( -. T e. _V -> R = (/) )
38 37 mpteq1d 
 |-  ( -. T e. _V -> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) = ( e e. (/) |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) )
39 mpt0 
 |-  ( e e. (/) |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) = (/)
40 38 39 eqtrdi 
 |-  ( -. T e. _V -> ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) = (/) )
41 32 35 40 3eqtr4a 
 |-  ( -. T e. _V -> ( S ` F ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) )
42 41 a1d 
 |-  ( -. T e. _V -> ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) ) )
43 31 42 pm2.61i 
 |-  ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) )