Metamath Proof Explorer

Theorem elmrsubrn

Description: Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses ( C \ V ) because we don't know that C and V are disjoint until we get to ismfs .) (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubccat.s 
|- S = ( mRSubst ` T )
mrsubccat.r 
|- R = ( mREx ` T )
mrsubcn.v 
|- V = ( mVR ` T )
mrsubcn.c 
|- C = ( mCN ` T )
Assertion elmrsubrn 
|- ( T e. W -> ( F e. ran S <-> ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. 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 mrsubcn.v 
 |-  V = ( mVR ` T )
4 mrsubcn.c 
 |-  C = ( mCN ` T )
5 1 2 mrsubf 
 |-  ( F e. ran S -> F : R --> R )
6 1 2 3 4 mrsubcn 
 |-  ( ( F e. ran S /\ c e. ( C \ V ) ) -> ( F ` <" c "> ) = <" c "> )
7 6 ralrimiva 
 |-  ( F e. ran S -> A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> )
8 1 2 mrsubccat 
 |-  ( ( F e. ran S /\ x e. R /\ y e. R ) -> ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) )
9 8 3expb 
 |-  ( ( F e. ran S /\ ( x e. R /\ y e. R ) ) -> ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) )
10 9 ralrimivva 
 |-  ( F e. ran S -> A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) )
11 5 7 10 3jca 
 |-  ( F e. ran S -> ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) )
12 4 3 2 mrexval 
 |-  ( T e. W -> R = Word ( C u. V ) )
13 12 adantr 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> R = Word ( C u. V ) )
14 s1eq 
 |-  ( w = v -> <" w "> = <" v "> )
15 14 fveq2d 
 |-  ( w = v -> ( F ` <" w "> ) = ( F ` <" v "> ) )
16 eqid 
 |-  ( w e. V |-> ( F ` <" w "> ) ) = ( w e. V |-> ( F ` <" w "> ) )
17 fvex 
 |-  ( F ` <" v "> ) e. _V
18 15 16 17 fvmpt 
 |-  ( v e. V -> ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) = ( F ` <" v "> ) )
19 18 adantl 
 |-  ( ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) /\ v e. V ) -> ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) = ( F ` <" v "> ) )
20 difun2 
 |-  ( ( C u. V ) \ V ) = ( C \ V )
21 20 eleq2i 
 |-  ( v e. ( ( C u. V ) \ V ) <-> v e. ( C \ V ) )
22 eldif 
 |-  ( v e. ( ( C u. V ) \ V ) <-> ( v e. ( C u. V ) /\ -. v e. V ) )
23 21 22 bitr3i 
 |-  ( v e. ( C \ V ) <-> ( v e. ( C u. V ) /\ -. v e. V ) )
24 simpr2 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> )
25 s1eq 
 |-  ( c = v -> <" c "> = <" v "> )
26 25 fveq2d 
 |-  ( c = v -> ( F ` <" c "> ) = ( F ` <" v "> ) )
27 26 25 eqeq12d 
 |-  ( c = v -> ( ( F ` <" c "> ) = <" c "> <-> ( F ` <" v "> ) = <" v "> ) )
28 27 rspccva 
 |-  ( ( A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ v e. ( C \ V ) ) -> ( F ` <" v "> ) = <" v "> )
29 24 28 sylan 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C \ V ) ) -> ( F ` <" v "> ) = <" v "> )
30 23 29 sylan2br 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ ( v e. ( C u. V ) /\ -. v e. V ) ) -> ( F ` <" v "> ) = <" v "> )
31 30 anassrs 
 |-  ( ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) /\ -. v e. V ) -> ( F ` <" v "> ) = <" v "> )
32 31 eqcomd 
 |-  ( ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) /\ -. v e. V ) -> <" v "> = ( F ` <" v "> ) )
33 19 32 ifeqda 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) -> if ( v e. V , ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) , <" v "> ) = ( F ` <" v "> ) )
34 33 mpteq2dva 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( v e. ( C u. V ) |-> if ( v e. V , ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) , <" v "> ) ) = ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) )
35 34 coeq1d 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( ( v e. ( C u. V ) |-> if ( v e. V , ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) , <" v "> ) ) o. r ) = ( ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) o. r ) )
36 35 oveq2d 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> if ( v e. V , ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) , <" v "> ) ) o. r ) ) = ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) o. r ) ) )
37 13 36 mpteq12dv 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( r e. R |-> ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> if ( v e. V , ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) , <" v "> ) ) o. r ) ) ) = ( r e. Word ( C u. V ) |-> ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) o. r ) ) ) )
38 elun2 
 |-  ( v e. V -> v e. ( C u. V ) )
39 simplr1 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) -> F : R --> R )
40 simpr 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) -> v e. ( C u. V ) )
41 40 s1cld 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) -> <" v "> e. Word ( C u. V ) )
42 12 ad2antrr 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) -> R = Word ( C u. V ) )
43 41 42 eleqtrrd 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) -> <" v "> e. R )
44 39 43 ffvelrnd 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) -> ( F ` <" v "> ) e. R )
45 38 44 sylan2 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. V ) -> ( F ` <" v "> ) e. R )
46 15 cbvmptv 
 |-  ( w e. V |-> ( F ` <" w "> ) ) = ( v e. V |-> ( F ` <" v "> ) )
47 45 46 fmptd 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( w e. V |-> ( F ` <" w "> ) ) : V --> R )
48 ssid 
 |-  V C_ V
49 eqid 
 |-  ( freeMnd ` ( C u. V ) ) = ( freeMnd ` ( C u. V ) )
50 4 3 2 1 49 mrsubfval 
 |-  ( ( ( w e. V |-> ( F ` <" w "> ) ) : V --> R /\ V C_ V ) -> ( S ` ( w e. V |-> ( F ` <" w "> ) ) ) = ( r e. R |-> ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> if ( v e. V , ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) , <" v "> ) ) o. r ) ) ) )
51 47 48 50 sylancl 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( S ` ( w e. V |-> ( F ` <" w "> ) ) ) = ( r e. R |-> ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> if ( v e. V , ( ( w e. V |-> ( F ` <" w "> ) ) ` v ) , <" v "> ) ) o. r ) ) ) )
52 4 fvexi 
 |-  C e. _V
53 3 fvexi 
 |-  V e. _V
54 52 53 unex 
 |-  ( C u. V ) e. _V
55 49 frmdmnd 
 |-  ( ( C u. V ) e. _V -> ( freeMnd ` ( C u. V ) ) e. Mnd )
56 54 55 ax-mp 
 |-  ( freeMnd ` ( C u. V ) ) e. Mnd
57 56 a1i 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( freeMnd ` ( C u. V ) ) e. Mnd )
58 54 a1i 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( C u. V ) e. _V )
59 44 42 eleqtrd 
 |-  ( ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) /\ v e. ( C u. V ) ) -> ( F ` <" v "> ) e. Word ( C u. V ) )
60 59 fmpttd 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) : ( C u. V ) --> Word ( C u. V ) )
61 simpr1 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> F : R --> R )
62 13 13 feq23d 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( F : R --> R <-> F : Word ( C u. V ) --> Word ( C u. V ) ) )
63 61 62 mpbid 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> F : Word ( C u. V ) --> Word ( C u. V ) )
64 simpr3 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) )
65 simprl 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> x e. R )
66 12 adantr 
 |-  ( ( T e. W /\ F : R --> R ) -> R = Word ( C u. V ) )
67 66 adantr 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> R = Word ( C u. V ) )
68 65 67 eleqtrd 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> x e. Word ( C u. V ) )
69 simprr 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> y e. R )
70 69 67 eleqtrd 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> y e. Word ( C u. V ) )
71 eqid 
 |-  ( Base ` ( freeMnd ` ( C u. V ) ) ) = ( Base ` ( freeMnd ` ( C u. V ) ) )
72 49 71 frmdbas 
 |-  ( ( C u. V ) e. _V -> ( Base ` ( freeMnd ` ( C u. V ) ) ) = Word ( C u. V ) )
73 54 72 ax-mp 
 |-  ( Base ` ( freeMnd ` ( C u. V ) ) ) = Word ( C u. V )
74 73 eqcomi 
 |-  Word ( C u. V ) = ( Base ` ( freeMnd ` ( C u. V ) ) )
75 eqid 
 |-  ( +g ` ( freeMnd ` ( C u. V ) ) ) = ( +g ` ( freeMnd ` ( C u. V ) ) )
76 49 74 75 frmdadd 
 |-  ( ( x e. Word ( C u. V ) /\ y e. Word ( C u. V ) ) -> ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) = ( x ++ y ) )
77 68 70 76 syl2anc 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) = ( x ++ y ) )
78 77 fveq2d 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( F ` ( x ++ y ) ) )
79 ffvelrn 
 |-  ( ( F : R --> R /\ x e. R ) -> ( F ` x ) e. R )
80 79 ad2ant2lr 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> ( F ` x ) e. R )
81 80 67 eleqtrd 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> ( F ` x ) e. Word ( C u. V ) )
82 ffvelrn 
 |-  ( ( F : R --> R /\ y e. R ) -> ( F ` y ) e. R )
83 82 ad2ant2l 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> ( F ` y ) e. R )
84 83 67 eleqtrd 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> ( F ` y ) e. Word ( C u. V ) )
85 49 74 75 frmdadd 
 |-  ( ( ( F ` x ) e. Word ( C u. V ) /\ ( F ` y ) e. Word ( C u. V ) ) -> ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) = ( ( F ` x ) ++ ( F ` y ) ) )
86 81 84 85 syl2anc 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) = ( ( F ` x ) ++ ( F ` y ) ) )
87 78 86 eqeq12d 
 |-  ( ( ( T e. W /\ F : R --> R ) /\ ( x e. R /\ y e. R ) ) -> ( ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) <-> ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) )
88 87 2ralbidva 
 |-  ( ( T e. W /\ F : R --> R ) -> ( A. x e. R A. y e. R ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) <-> A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) )
89 66 raleqdv 
 |-  ( ( T e. W /\ F : R --> R ) -> ( A. y e. R ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) <-> A. y e. Word ( C u. V ) ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) ) )
90 66 89 raleqbidv 
 |-  ( ( T e. W /\ F : R --> R ) -> ( A. x e. R A. y e. R ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) <-> A. x e. Word ( C u. V ) A. y e. Word ( C u. V ) ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) ) )
91 88 90 bitr3d 
 |-  ( ( T e. W /\ F : R --> R ) -> ( A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) <-> A. x e. Word ( C u. V ) A. y e. Word ( C u. V ) ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) ) )
92 91 3ad2antr1 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) <-> A. x e. Word ( C u. V ) A. y e. Word ( C u. V ) ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) ) )
93 64 92 mpbid 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> A. x e. Word ( C u. V ) A. y e. Word ( C u. V ) ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) )
94 wrd0 
 |-  (/) e. Word ( C u. V )
95 ffvelrn 
 |-  ( ( F : Word ( C u. V ) --> Word ( C u. V ) /\ (/) e. Word ( C u. V ) ) -> ( F ` (/) ) e. Word ( C u. V ) )
96 63 94 95 sylancl 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( F ` (/) ) e. Word ( C u. V ) )
97 lencl 
 |-  ( ( F ` (/) ) e. Word ( C u. V ) -> ( # ` ( F ` (/) ) ) e. NN0 )
98 96 97 syl 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( # ` ( F ` (/) ) ) e. NN0 )
99 98 nn0cnd 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( # ` ( F ` (/) ) ) e. CC )
100 0cnd 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> 0 e. CC )
101 99 addid1d 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( ( # ` ( F ` (/) ) ) + 0 ) = ( # ` ( F ` (/) ) ) )
102 94 13 eleqtrrid 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> (/) e. R )
103 fvoveq1 
 |-  ( x = (/) -> ( F ` ( x ++ y ) ) = ( F ` ( (/) ++ y ) ) )
104 fveq2 
 |-  ( x = (/) -> ( F ` x ) = ( F ` (/) ) )
105 104 oveq1d 
 |-  ( x = (/) -> ( ( F ` x ) ++ ( F ` y ) ) = ( ( F ` (/) ) ++ ( F ` y ) ) )
106 103 105 eqeq12d 
 |-  ( x = (/) -> ( ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) <-> ( F ` ( (/) ++ y ) ) = ( ( F ` (/) ) ++ ( F ` y ) ) ) )
107 oveq2 
 |-  ( y = (/) -> ( (/) ++ y ) = ( (/) ++ (/) ) )
108 ccatidid 
 |-  ( (/) ++ (/) ) = (/)
109 107 108 eqtrdi 
 |-  ( y = (/) -> ( (/) ++ y ) = (/) )
110 109 fveq2d 
 |-  ( y = (/) -> ( F ` ( (/) ++ y ) ) = ( F ` (/) ) )
111 fveq2 
 |-  ( y = (/) -> ( F ` y ) = ( F ` (/) ) )
112 111 oveq2d 
 |-  ( y = (/) -> ( ( F ` (/) ) ++ ( F ` y ) ) = ( ( F ` (/) ) ++ ( F ` (/) ) ) )
113 110 112 eqeq12d 
 |-  ( y = (/) -> ( ( F ` ( (/) ++ y ) ) = ( ( F ` (/) ) ++ ( F ` y ) ) <-> ( F ` (/) ) = ( ( F ` (/) ) ++ ( F ` (/) ) ) ) )
114 106 113 rspc2va 
 |-  ( ( ( (/) e. R /\ (/) e. R ) /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) -> ( F ` (/) ) = ( ( F ` (/) ) ++ ( F ` (/) ) ) )
115 102 102 64 114 syl21anc 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( F ` (/) ) = ( ( F ` (/) ) ++ ( F ` (/) ) ) )
116 115 fveq2d 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( # ` ( F ` (/) ) ) = ( # ` ( ( F ` (/) ) ++ ( F ` (/) ) ) ) )
117 ccatlen 
 |-  ( ( ( F ` (/) ) e. Word ( C u. V ) /\ ( F ` (/) ) e. Word ( C u. V ) ) -> ( # ` ( ( F ` (/) ) ++ ( F ` (/) ) ) ) = ( ( # ` ( F ` (/) ) ) + ( # ` ( F ` (/) ) ) ) )
118 96 96 117 syl2anc 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( # ` ( ( F ` (/) ) ++ ( F ` (/) ) ) ) = ( ( # ` ( F ` (/) ) ) + ( # ` ( F ` (/) ) ) ) )
119 101 116 118 3eqtrrd 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( ( # ` ( F ` (/) ) ) + ( # ` ( F ` (/) ) ) ) = ( ( # ` ( F ` (/) ) ) + 0 ) )
120 99 99 100 119 addcanad 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( # ` ( F ` (/) ) ) = 0 )
121 fvex 
 |-  ( F ` (/) ) e. _V
122 hasheq0 
 |-  ( ( F ` (/) ) e. _V -> ( ( # ` ( F ` (/) ) ) = 0 <-> ( F ` (/) ) = (/) ) )
123 121 122 ax-mp 
 |-  ( ( # ` ( F ` (/) ) ) = 0 <-> ( F ` (/) ) = (/) )
124 120 123 sylib 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( F ` (/) ) = (/) )
125 56 56 pm3.2i 
 |-  ( ( freeMnd ` ( C u. V ) ) e. Mnd /\ ( freeMnd ` ( C u. V ) ) e. Mnd )
126 49 frmd0 
 |-  (/) = ( 0g ` ( freeMnd ` ( C u. V ) ) )
127 74 74 75 75 126 126 ismhm 
 |-  ( F e. ( ( freeMnd ` ( C u. V ) ) MndHom ( freeMnd ` ( C u. V ) ) ) <-> ( ( ( freeMnd ` ( C u. V ) ) e. Mnd /\ ( freeMnd ` ( C u. V ) ) e. Mnd ) /\ ( F : Word ( C u. V ) --> Word ( C u. V ) /\ A. x e. Word ( C u. V ) A. y e. Word ( C u. V ) ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) /\ ( F ` (/) ) = (/) ) ) )
128 125 127 mpbiran 
 |-  ( F e. ( ( freeMnd ` ( C u. V ) ) MndHom ( freeMnd ` ( C u. V ) ) ) <-> ( F : Word ( C u. V ) --> Word ( C u. V ) /\ A. x e. Word ( C u. V ) A. y e. Word ( C u. V ) ( F ` ( x ( +g ` ( freeMnd ` ( C u. V ) ) ) y ) ) = ( ( F ` x ) ( +g ` ( freeMnd ` ( C u. V ) ) ) ( F ` y ) ) /\ ( F ` (/) ) = (/) ) )
129 63 93 124 128 syl3anbrc 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> F e. ( ( freeMnd ` ( C u. V ) ) MndHom ( freeMnd ` ( C u. V ) ) ) )
130 eqid 
 |-  ( varFMnd ` ( C u. V ) ) = ( varFMnd ` ( C u. V ) )
131 130 vrmdf 
 |-  ( ( C u. V ) e. _V -> ( varFMnd ` ( C u. V ) ) : ( C u. V ) --> Word ( C u. V ) )
132 54 131 ax-mp 
 |-  ( varFMnd ` ( C u. V ) ) : ( C u. V ) --> Word ( C u. V )
133 fcompt 
 |-  ( ( F : Word ( C u. V ) --> Word ( C u. V ) /\ ( varFMnd ` ( C u. V ) ) : ( C u. V ) --> Word ( C u. V ) ) -> ( F o. ( varFMnd ` ( C u. V ) ) ) = ( v e. ( C u. V ) |-> ( F ` ( ( varFMnd ` ( C u. V ) ) ` v ) ) ) )
134 63 132 133 sylancl 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( F o. ( varFMnd ` ( C u. V ) ) ) = ( v e. ( C u. V ) |-> ( F ` ( ( varFMnd ` ( C u. V ) ) ` v ) ) ) )
135 130 vrmdval 
 |-  ( ( ( C u. V ) e. _V /\ v e. ( C u. V ) ) -> ( ( varFMnd ` ( C u. V ) ) ` v ) = <" v "> )
136 54 135 mpan 
 |-  ( v e. ( C u. V ) -> ( ( varFMnd ` ( C u. V ) ) ` v ) = <" v "> )
137 136 fveq2d 
 |-  ( v e. ( C u. V ) -> ( F ` ( ( varFMnd ` ( C u. V ) ) ` v ) ) = ( F ` <" v "> ) )
138 137 mpteq2ia 
 |-  ( v e. ( C u. V ) |-> ( F ` ( ( varFMnd ` ( C u. V ) ) ` v ) ) ) = ( v e. ( C u. V ) |-> ( F ` <" v "> ) )
139 134 138 eqtrdi 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( F o. ( varFMnd ` ( C u. V ) ) ) = ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) )
140 49 74 130 frmdup3lem 
 |-  ( ( ( ( freeMnd ` ( C u. V ) ) e. Mnd /\ ( C u. V ) e. _V /\ ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) : ( C u. V ) --> Word ( C u. V ) ) /\ ( F e. ( ( freeMnd ` ( C u. V ) ) MndHom ( freeMnd ` ( C u. V ) ) ) /\ ( F o. ( varFMnd ` ( C u. V ) ) ) = ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) ) ) -> F = ( r e. Word ( C u. V ) |-> ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) o. r ) ) ) )
141 57 58 60 129 139 140 syl32anc 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> F = ( r e. Word ( C u. V ) |-> ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> ( F ` <" v "> ) ) o. r ) ) ) )
142 37 51 141 3eqtr4rd 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> F = ( S ` ( w e. V |-> ( F ` <" w "> ) ) ) )
143 3 2 1 mrsubff 
 |-  ( T e. W -> S : ( R ^pm V ) --> ( R ^m R ) )
144 143 ffnd 
 |-  ( T e. W -> S Fn ( R ^pm V ) )
145 144 adantr 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> S Fn ( R ^pm V ) )
146 2 fvexi 
 |-  R e. _V
147 elpm2r 
 |-  ( ( ( R e. _V /\ V e. _V ) /\ ( ( w e. V |-> ( F ` <" w "> ) ) : V --> R /\ V C_ V ) ) -> ( w e. V |-> ( F ` <" w "> ) ) e. ( R ^pm V ) )
148 146 53 147 mpanl12 
 |-  ( ( ( w e. V |-> ( F ` <" w "> ) ) : V --> R /\ V C_ V ) -> ( w e. V |-> ( F ` <" w "> ) ) e. ( R ^pm V ) )
149 47 48 148 sylancl 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( w e. V |-> ( F ` <" w "> ) ) e. ( R ^pm V ) )
150 fnfvelrn 
 |-  ( ( S Fn ( R ^pm V ) /\ ( w e. V |-> ( F ` <" w "> ) ) e. ( R ^pm V ) ) -> ( S ` ( w e. V |-> ( F ` <" w "> ) ) ) e. ran S )
151 145 149 150 syl2anc 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> ( S ` ( w e. V |-> ( F ` <" w "> ) ) ) e. ran S )
152 142 151 eqeltrd 
 |-  ( ( T e. W /\ ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) -> F e. ran S )
153 152 ex 
 |-  ( T e. W -> ( ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) -> F e. ran S ) )
154 11 153 impbid2 
 |-  ( T e. W -> ( F e. ran S <-> ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) )