# 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 ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) )`