Metamath Proof Explorer

Theorem mrsubccat

Description: Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubccat.s 
|- S = ( mRSubst ` T )
mrsubccat.r 
|- R = ( mREx ` T )
Assertion mrsubccat 
|- ( ( F e. ran S /\ X e. R /\ Y e. R ) -> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 mrsubccat.s 
 |-  S = ( mRSubst ` T )
2 mrsubccat.r 
 |-  R = ( mREx ` T )
3 n0i 
 |-  ( F e. ran S -> -. ran S = (/) )
4 1 rnfvprc 
 |-  ( -. T e. _V -> ran S = (/) )
5 3 4 nsyl2 
 |-  ( F e. ran S -> T e. _V )
6 eqid 
 |-  ( mVR ` T ) = ( mVR ` T )
7 6 2 1 mrsubff 
 |-  ( T e. _V -> S : ( R ^pm ( mVR ` T ) ) --> ( R ^m R ) )
8 ffun 
 |-  ( S : ( R ^pm ( mVR ` T ) ) --> ( R ^m R ) -> Fun S )
9 5 7 8 3syl 
 |-  ( F e. ran S -> Fun S )
10 6 2 1 mrsubrn 
 |-  ran S = ( S " ( R ^m ( mVR ` T ) ) )
11 10 eleq2i 
 |-  ( F e. ran S <-> F e. ( S " ( R ^m ( mVR ` T ) ) ) )
12 11 biimpi 
 |-  ( F e. ran S -> F e. ( S " ( R ^m ( mVR ` T ) ) ) )
13 fvelima 
 |-  ( ( Fun S /\ F e. ( S " ( R ^m ( mVR ` T ) ) ) ) -> E. f e. ( R ^m ( mVR ` T ) ) ( S ` f ) = F )
14 9 12 13 syl2anc 
 |-  ( F e. ran S -> E. f e. ( R ^m ( mVR ` T ) ) ( S ` f ) = F )
15 simprl 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> X e. R )
16 elfvex 
 |-  ( X e. ( mREx ` T ) -> T e. _V )
17 16 2 eleq2s 
 |-  ( X e. R -> T e. _V )
18 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
19 18 6 2 mrexval 
 |-  ( T e. _V -> R = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
20 15 17 19 3syl 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> R = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
21 15 20 eleqtrd 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> X e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
22 simprr 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> Y e. R )
23 22 20 eleqtrd 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> Y e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
24 elmapi 
 |-  ( f e. ( R ^m ( mVR ` T ) ) -> f : ( mVR ` T ) --> R )
25 24 adantr 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> f : ( mVR ` T ) --> R )
26 25 adantr 
 |-  ( ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) /\ v e. ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> f : ( mVR ` T ) --> R )
27 26 ffvelrnda 
 |-  ( ( ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) /\ v e. ( ( mCN ` T ) u. ( mVR ` T ) ) ) /\ v e. ( mVR ` T ) ) -> ( f ` v ) e. R )
28 20 ad2antrr 
 |-  ( ( ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) /\ v e. ( ( mCN ` T ) u. ( mVR ` T ) ) ) /\ v e. ( mVR ` T ) ) -> R = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
29 27 28 eleqtrd 
 |-  ( ( ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) /\ v e. ( ( mCN ` T ) u. ( mVR ` T ) ) ) /\ v e. ( mVR ` T ) ) -> ( f ` v ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
30 simplr 
 |-  ( ( ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) /\ v e. ( ( mCN ` T ) u. ( mVR ` T ) ) ) /\ -. v e. ( mVR ` T ) ) -> v e. ( ( mCN ` T ) u. ( mVR ` T ) ) )
31 30 s1cld 
 |-  ( ( ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) /\ v e. ( ( mCN ` T ) u. ( mVR ` T ) ) ) /\ -. v e. ( mVR ` T ) ) -> <" v "> e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
32 29 31 ifclda 
 |-  ( ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) /\ v e. ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
33 32 fmpttd 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) : ( ( mCN ` T ) u. ( mVR ` T ) ) --> Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
34 ccatco 
 |-  ( ( X e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) /\ Y e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) /\ ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) : ( ( mCN ` T ) u. ( mVR ` T ) ) --> Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. ( X ++ Y ) ) = ( ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ++ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) )
35 21 23 33 34 syl3anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. ( X ++ Y ) ) = ( ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ++ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) )
36 35 oveq2d 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. ( X ++ Y ) ) ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ++ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) )
37 fvex 
 |-  ( mCN ` T ) e. _V
38 fvex 
 |-  ( mVR ` T ) e. _V
39 37 38 unex 
 |-  ( ( mCN ` T ) u. ( mVR ` T ) ) e. _V
40 eqid 
 |-  ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) = ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) )
41 40 frmdmnd 
 |-  ( ( ( mCN ` T ) u. ( mVR ` T ) ) e. _V -> ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) e. Mnd )
42 39 41 mp1i 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) e. Mnd )
43 wrdco 
 |-  ( ( X e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) /\ ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) : ( ( mCN ` T ) u. ( mVR ` T ) ) --> Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) e. Word Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
44 21 33 43 syl2anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) e. Word Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
45 wrdco 
 |-  ( ( Y e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) /\ ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) : ( ( mCN ` T ) u. ( mVR ` T ) ) --> Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) e. Word Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
46 23 33 45 syl2anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) e. Word Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
47 eqid 
 |-  ( Base ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) ) = ( Base ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) )
48 40 47 frmdbas 
 |-  ( ( ( mCN ` T ) u. ( mVR ` T ) ) e. _V -> ( Base ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
49 39 48 ax-mp 
 |-  ( Base ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) ) = Word ( ( mCN ` T ) u. ( mVR ` T ) )
50 49 eqcomi 
 |-  Word ( ( mCN ` T ) u. ( mVR ` T ) ) = ( Base ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) )
51 eqid 
 |-  ( +g ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) ) = ( +g ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) )
52 50 51 gsumccat 
 |-  ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) e. Mnd /\ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) e. Word Word ( ( mCN ` T ) u. ( mVR ` T ) ) /\ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) e. Word Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ++ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) = ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) ( +g ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) ) ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) )
53 42 44 46 52 syl3anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ++ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) = ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) ( +g ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) ) ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) )
54 50 gsumwcl 
 |-  ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) e. Mnd /\ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) e. Word Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
55 42 44 54 syl2anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
56 50 gsumwcl 
 |-  ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) e. Mnd /\ ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) e. Word Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
57 42 46 56 syl2anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
58 40 50 51 frmdadd 
 |-  ( ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) /\ ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) ( +g ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) ) ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) = ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) ++ ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) )
59 55 57 58 syl2anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) ( +g ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) ) ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) = ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) ++ ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) )
60 36 53 59 3eqtrd 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. ( X ++ Y ) ) ) = ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) ++ ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) )
61 ssidd 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( mVR ` T ) C_ ( mVR ` T ) )
62 ccatcl 
 |-  ( ( X e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) /\ Y e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( X ++ Y ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
63 21 23 62 syl2anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( X ++ Y ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
64 63 20 eleqtrrd 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( X ++ Y ) e. R )
65 18 6 2 1 40 mrsubval 
 |-  ( ( f : ( mVR ` T ) --> R /\ ( mVR ` T ) C_ ( mVR ` T ) /\ ( X ++ Y ) e. R ) -> ( ( S ` f ) ` ( X ++ Y ) ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. ( X ++ Y ) ) ) )
66 25 61 64 65 syl3anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( S ` f ) ` ( X ++ Y ) ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. ( X ++ Y ) ) ) )
67 18 6 2 1 40 mrsubval 
 |-  ( ( f : ( mVR ` T ) --> R /\ ( mVR ` T ) C_ ( mVR ` T ) /\ X e. R ) -> ( ( S ` f ) ` X ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) )
68 25 61 15 67 syl3anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( S ` f ) ` X ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) )
69 18 6 2 1 40 mrsubval 
 |-  ( ( f : ( mVR ` T ) --> R /\ ( mVR ` T ) C_ ( mVR ` T ) /\ Y e. R ) -> ( ( S ` f ) ` Y ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) )
70 25 61 22 69 syl3anc 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( S ` f ) ` Y ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) )
71 68 70 oveq12d 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( ( S ` f ) ` X ) ++ ( ( S ` f ) ` Y ) ) = ( ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. X ) ) ++ ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. Y ) ) ) )
72 60 66 71 3eqtr4d 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( S ` f ) ` ( X ++ Y ) ) = ( ( ( S ` f ) ` X ) ++ ( ( S ` f ) ` Y ) ) )
73 fveq1 
 |-  ( ( S ` f ) = F -> ( ( S ` f ) ` ( X ++ Y ) ) = ( F ` ( X ++ Y ) ) )
74 fveq1 
 |-  ( ( S ` f ) = F -> ( ( S ` f ) ` X ) = ( F ` X ) )
75 fveq1 
 |-  ( ( S ` f ) = F -> ( ( S ` f ) ` Y ) = ( F ` Y ) )
76 74 75 oveq12d 
 |-  ( ( S ` f ) = F -> ( ( ( S ` f ) ` X ) ++ ( ( S ` f ) ` Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) )
77 73 76 eqeq12d 
 |-  ( ( S ` f ) = F -> ( ( ( S ` f ) ` ( X ++ Y ) ) = ( ( ( S ` f ) ` X ) ++ ( ( S ` f ) ` Y ) ) <-> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) ) )
78 72 77 syl5ibcom 
 |-  ( ( f e. ( R ^m ( mVR ` T ) ) /\ ( X e. R /\ Y e. R ) ) -> ( ( S ` f ) = F -> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) ) )
79 78 ex 
 |-  ( f e. ( R ^m ( mVR ` T ) ) -> ( ( X e. R /\ Y e. R ) -> ( ( S ` f ) = F -> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) ) ) )
80 79 com23 
 |-  ( f e. ( R ^m ( mVR ` T ) ) -> ( ( S ` f ) = F -> ( ( X e. R /\ Y e. R ) -> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) ) ) )
81 80 rexlimiv 
 |-  ( E. f e. ( R ^m ( mVR ` T ) ) ( S ` f ) = F -> ( ( X e. R /\ Y e. R ) -> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) ) )
82 14 81 syl 
 |-  ( F e. ran S -> ( ( X e. R /\ Y e. R ) -> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) ) )
83 82 3impib 
 |-  ( ( F e. ran S /\ X e. R /\ Y e. R ) -> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) )