Metamath Proof Explorer

Theorem mrsubff

Description: A substitution is a function from R to R . (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubvr.v 
|- V = ( mVR ` T )
mrsubvr.r 
|- R = ( mREx ` T )
mrsubvr.s 
|- S = ( mRSubst ` T )
Assertion mrsubff 
|- ( T e. W -> S : ( R ^pm V ) --> ( R ^m R ) )

Proof

Step Hyp Ref Expression
1 mrsubvr.v 
 |-  V = ( mVR ` T )
2 mrsubvr.r 
 |-  R = ( mREx ` T )
3 mrsubvr.s 
 |-  S = ( mRSubst ` T )
4 fvex 
 |-  ( mCN ` T ) e. _V
5 1 fvexi 
 |-  V e. _V
6 4 5 unex 
 |-  ( ( mCN ` T ) u. V ) e. _V
7 eqid 
 |-  ( freeMnd ` ( ( mCN ` T ) u. V ) ) = ( freeMnd ` ( ( mCN ` T ) u. V ) )
8 7 frmdmnd 
 |-  ( ( ( mCN ` T ) u. V ) e. _V -> ( freeMnd ` ( ( mCN ` T ) u. V ) ) e. Mnd )
9 6 8 mp1i 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) -> ( freeMnd ` ( ( mCN ` T ) u. V ) ) e. Mnd )
10 simpr 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) -> e e. R )
11 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
12 11 1 2 mrexval 
 |-  ( T e. W -> R = Word ( ( mCN ` T ) u. V ) )
13 12 ad2antrr 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) -> R = Word ( ( mCN ` T ) u. V ) )
14 10 13 eleqtrd 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) -> e e. Word ( ( mCN ` T ) u. V ) )
15 elpmi 
 |-  ( f e. ( R ^pm V ) -> ( f : dom f --> R /\ dom f C_ V ) )
16 15 simpld 
 |-  ( f e. ( R ^pm V ) -> f : dom f --> R )
17 16 ad3antlr 
 |-  ( ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) /\ v e. ( ( mCN ` T ) u. V ) ) -> f : dom f --> R )
18 17 ffvelrnda 
 |-  ( ( ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) /\ v e. ( ( mCN ` T ) u. V ) ) /\ v e. dom f ) -> ( f ` v ) e. R )
19 13 ad2antrr 
 |-  ( ( ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) /\ v e. ( ( mCN ` T ) u. V ) ) /\ v e. dom f ) -> R = Word ( ( mCN ` T ) u. V ) )
20 18 19 eleqtrd 
 |-  ( ( ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) /\ v e. ( ( mCN ` T ) u. V ) ) /\ v e. dom f ) -> ( f ` v ) e. Word ( ( mCN ` T ) u. V ) )
21 simplr 
 |-  ( ( ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) /\ v e. ( ( mCN ` T ) u. V ) ) /\ -. v e. dom f ) -> v e. ( ( mCN ` T ) u. V ) )
22 21 s1cld 
 |-  ( ( ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) /\ v e. ( ( mCN ` T ) u. V ) ) /\ -. v e. dom f ) -> <" v "> e. Word ( ( mCN ` T ) u. V ) )
23 20 22 ifclda 
 |-  ( ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) /\ v e. ( ( mCN ` T ) u. V ) ) -> if ( v e. dom f , ( f ` v ) , <" v "> ) e. Word ( ( mCN ` T ) u. V ) )
24 23 fmpttd 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) -> ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) : ( ( mCN ` T ) u. V ) --> Word ( ( mCN ` T ) u. V ) )
25 wrdco 
 |-  ( ( e e. Word ( ( mCN ` T ) u. V ) /\ ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) : ( ( mCN ` T ) u. V ) --> Word ( ( mCN ` T ) u. V ) ) -> ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) e. Word Word ( ( mCN ` T ) u. V ) )
26 14 24 25 syl2anc 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) -> ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) e. Word Word ( ( mCN ` T ) u. V ) )
27 eqid 
 |-  ( Base ` ( freeMnd ` ( ( mCN ` T ) u. V ) ) ) = ( Base ` ( freeMnd ` ( ( mCN ` T ) u. V ) ) )
28 7 27 frmdbas 
 |-  ( ( ( mCN ` T ) u. V ) e. _V -> ( Base ` ( freeMnd ` ( ( mCN ` T ) u. V ) ) ) = Word ( ( mCN ` T ) u. V ) )
29 6 28 ax-mp 
 |-  ( Base ` ( freeMnd ` ( ( mCN ` T ) u. V ) ) ) = Word ( ( mCN ` T ) u. V )
30 29 eqcomi 
 |-  Word ( ( mCN ` T ) u. V ) = ( Base ` ( freeMnd ` ( ( mCN ` T ) u. V ) ) )
31 30 gsumwcl 
 |-  ( ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) e. Mnd /\ ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) e. Word Word ( ( mCN ` T ) u. V ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) e. Word ( ( mCN ` T ) u. V ) )
32 9 26 31 syl2anc 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) -> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) e. Word ( ( mCN ` T ) u. V ) )
33 32 13 eleqtrrd 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. R ) -> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) e. R )
34 33 fmpttd 
 |-  ( ( T e. W /\ f e. ( R ^pm V ) ) -> ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) : R --> R )
35 2 fvexi 
 |-  R e. _V
36 35 35 elmap 
 |-  ( ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) e. ( R ^m R ) <-> ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) : R --> R )
37 34 36 sylibr 
 |-  ( ( T e. W /\ f e. ( R ^pm V ) ) -> ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) e. ( R ^m R ) )
38 37 fmpttd 
 |-  ( T e. W -> ( f e. ( R ^pm V ) |-> ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) : ( R ^pm V ) --> ( R ^m R ) )
39 11 1 2 3 7 mrsubffval 
 |-  ( T e. W -> S = ( f e. ( R ^pm V ) |-> ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )
40 39 feq1d 
 |-  ( T e. W -> ( S : ( R ^pm V ) --> ( R ^m R ) <-> ( f e. ( R ^pm V ) |-> ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) : ( R ^pm V ) --> ( R ^m R ) ) )
41 38 40 mpbird 
 |-  ( T e. W -> S : ( R ^pm V ) --> ( R ^m R ) )