Metamath Proof Explorer

Theorem cycpmco2lem5

Description: Lemma for cycpmco2 . (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c 
|- M = ( toCyc ` D )
cycpmco2.s 
|- S = ( SymGrp ` D )
cycpmco2.d 
|- ( ph -> D e. V )
cycpmco2.w 
|- ( ph -> W e. dom M )
cycpmco2.i 
|- ( ph -> I e. ( D \ ran W ) )
cycpmco2.j 
|- ( ph -> J e. ran W )
cycpmco2.e 
|- E = ( ( `' W ` J ) + 1 )
cycpmco2.1 
|- U = ( W splice <. E , E , <" I "> >. )
cycpmco2lem.1 
|- ( ph -> K e. ran W )
cycpmco2lem5.1 
|- ( ph -> ( `' U ` K ) = ( ( # ` U ) - 1 ) )
Assertion cycpmco2lem5 
|- ( ph -> ( ( M ` U ) ` K ) = ( ( M ` W ) ` K ) )

Proof

Step Hyp Ref Expression
1 cycpmco2.c 
 |-  M = ( toCyc ` D )
2 cycpmco2.s 
 |-  S = ( SymGrp ` D )
3 cycpmco2.d 
 |-  ( ph -> D e. V )
4 cycpmco2.w 
 |-  ( ph -> W e. dom M )
5 cycpmco2.i 
 |-  ( ph -> I e. ( D \ ran W ) )
6 cycpmco2.j 
 |-  ( ph -> J e. ran W )
7 cycpmco2.e 
 |-  E = ( ( `' W ` J ) + 1 )
8 cycpmco2.1 
 |-  U = ( W splice <. E , E , <" I "> >. )
9 cycpmco2lem.1 
 |-  ( ph -> K e. ran W )
10 cycpmco2lem5.1 
 |-  ( ph -> ( `' U ` K ) = ( ( # ` U ) - 1 ) )
11 9 adantr 
 |-  ( ( ph /\ ( # ` W ) = E ) -> K e. ran W )
12 ovexd 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. _V )
13 7 12 eqeltrid 
 |-  ( ph -> E e. _V )
14 5 eldifad 
 |-  ( ph -> I e. D )
15 14 s1cld 
 |-  ( ph -> <" I "> e. Word D )
16 splval 
 |-  ( ( W e. dom M /\ ( E e. _V /\ E e. _V /\ <" I "> e. Word D ) ) -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
17 4 13 13 15 16 syl13anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
18 8 17 eqtrid 
 |-  ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
19 18 fveq2d 
 |-  ( ph -> ( # ` U ) = ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) )
20 ssrab2 
 |-  { w e. Word D | w : dom w -1-1-> D } C_ Word D
21 eqid 
 |-  ( Base ` S ) = ( Base ` S )
22 1 2 21 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
23 3 22 syl 
 |-  ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
24 23 fdmd 
 |-  ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
25 4 24 eleqtrd 
 |-  ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
26 20 25 sselid 
 |-  ( ph -> W e. Word D )
27 pfxcl 
 |-  ( W e. Word D -> ( W prefix E ) e. Word D )
28 26 27 syl 
 |-  ( ph -> ( W prefix E ) e. Word D )
29 ccatcl 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
30 28 15 29 syl2anc 
 |-  ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
31 swrdcl 
 |-  ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
32 26 31 syl 
 |-  ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
33 ccatlen 
 |-  ( ( ( ( W prefix E ) ++ <" I "> ) e. Word D /\ ( W substr <. E , ( # ` W ) >. ) e. Word D ) -> ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) )
34 30 32 33 syl2anc 
 |-  ( ph -> ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) )
35 ccatws1len 
 |-  ( ( W prefix E ) e. Word D -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
36 28 35 syl 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
37 id 
 |-  ( w = W -> w = W )
38 dmeq 
 |-  ( w = W -> dom w = dom W )
39 eqidd 
 |-  ( w = W -> D = D )
40 37 38 39 f1eq123d 
 |-  ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
41 40 elrab 
 |-  ( W e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
42 25 41 sylib 
 |-  ( ph -> ( W e. Word D /\ W : dom W -1-1-> D ) )
43 42 simprd 
 |-  ( ph -> W : dom W -1-1-> D )
44 f1cnv 
 |-  ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
45 43 44 syl 
 |-  ( ph -> `' W : ran W -1-1-onto-> dom W )
46 f1of 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
47 45 46 syl 
 |-  ( ph -> `' W : ran W --> dom W )
48 47 6 ffvelcdmd 
 |-  ( ph -> ( `' W ` J ) e. dom W )
49 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
50 26 49 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
51 48 50 eleqtrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
52 fzofzp1 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
53 51 52 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
54 7 53 eqeltrid 
 |-  ( ph -> E e. ( 0 ... ( # ` W ) ) )
55 pfxlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix E ) ) = E )
56 26 54 55 syl2anc 
 |-  ( ph -> ( # ` ( W prefix E ) ) = E )
57 56 oveq1d 
 |-  ( ph -> ( ( # ` ( W prefix E ) ) + 1 ) = ( E + 1 ) )
58 36 57 eqtrd 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( E + 1 ) )
59 lencl 
 |-  ( W e. Word D -> ( # ` W ) e. NN0 )
60 26 59 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
61 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
62 60 61 sylib 
 |-  ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
63 swrdlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
64 26 54 62 63 syl3anc 
 |-  ( ph -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
65 58 64 oveq12d 
 |-  ( ph -> ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
66 19 34 65 3eqtrd 
 |-  ( ph -> ( # ` U ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
67 fz0ssnn0 
 |-  ( 0 ... ( # ` W ) ) C_ NN0
68 67 54 sselid 
 |-  ( ph -> E e. NN0 )
69 68 nn0zd 
 |-  ( ph -> E e. ZZ )
70 69 peano2zd 
 |-  ( ph -> ( E + 1 ) e. ZZ )
71 70 zcnd 
 |-  ( ph -> ( E + 1 ) e. CC )
72 60 nn0cnd 
 |-  ( ph -> ( # ` W ) e. CC )
73 68 nn0cnd 
 |-  ( ph -> E e. CC )
74 71 72 73 addsubassd 
 |-  ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
75 1cnd 
 |-  ( ph -> 1 e. CC )
76 73 75 72 addassd 
 |-  ( ph -> ( ( E + 1 ) + ( # ` W ) ) = ( E + ( 1 + ( # ` W ) ) ) )
77 76 oveq1d 
 |-  ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
78 66 74 77 3eqtr2d 
 |-  ( ph -> ( # ` U ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
79 75 72 addcld 
 |-  ( ph -> ( 1 + ( # ` W ) ) e. CC )
80 73 79 pncan2d 
 |-  ( ph -> ( ( E + ( 1 + ( # ` W ) ) ) - E ) = ( 1 + ( # ` W ) ) )
81 75 72 addcomd 
 |-  ( ph -> ( 1 + ( # ` W ) ) = ( ( # ` W ) + 1 ) )
82 78 80 81 3eqtrd 
 |-  ( ph -> ( # ` U ) = ( ( # ` W ) + 1 ) )
83 oveq1 
 |-  ( ( # ` W ) = E -> ( ( # ` W ) + 1 ) = ( E + 1 ) )
84 82 83 sylan9eq 
 |-  ( ( ph /\ ( # ` W ) = E ) -> ( # ` U ) = ( E + 1 ) )
85 84 oveq1d 
 |-  ( ( ph /\ ( # ` W ) = E ) -> ( ( # ` U ) - 1 ) = ( ( E + 1 ) - 1 ) )
86 73 75 pncand 
 |-  ( ph -> ( ( E + 1 ) - 1 ) = E )
87 86 adantr 
 |-  ( ( ph /\ ( # ` W ) = E ) -> ( ( E + 1 ) - 1 ) = E )
88 85 87 eqtrd 
 |-  ( ( ph /\ ( # ` W ) = E ) -> ( ( # ` U ) - 1 ) = E )
89 88 fveq2d 
 |-  ( ( ph /\ ( # ` W ) = E ) -> ( U ` ( ( # ` U ) - 1 ) ) = ( U ` E ) )
90 10 fveq2d 
 |-  ( ph -> ( U ` ( `' U ` K ) ) = ( U ` ( ( # ` U ) - 1 ) ) )
91 1 2 3 4 5 6 7 8 cycpmco2f1 
 |-  ( ph -> U : dom U -1-1-> D )
92 f1f1orn 
 |-  ( U : dom U -1-1-> D -> U : dom U -1-1-onto-> ran U )
93 91 92 syl 
 |-  ( ph -> U : dom U -1-1-onto-> ran U )
94 ssun1 
 |-  ran W C_ ( ran W u. { I } )
95 1 2 3 4 5 6 7 8 cycpmco2rn 
 |-  ( ph -> ran U = ( ran W u. { I } ) )
96 94 95 sseqtrrid 
 |-  ( ph -> ran W C_ ran U )
97 96 sselda 
 |-  ( ( ph /\ K e. ran W ) -> K e. ran U )
98 f1ocnvfv2 
 |-  ( ( U : dom U -1-1-onto-> ran U /\ K e. ran U ) -> ( U ` ( `' U ` K ) ) = K )
99 93 97 98 syl2an2r 
 |-  ( ( ph /\ K e. ran W ) -> ( U ` ( `' U ` K ) ) = K )
100 9 99 mpdan 
 |-  ( ph -> ( U ` ( `' U ` K ) ) = K )
101 90 100 eqtr3d 
 |-  ( ph -> ( U ` ( ( # ` U ) - 1 ) ) = K )
102 101 adantr 
 |-  ( ( ph /\ ( # ` W ) = E ) -> ( U ` ( ( # ` U ) - 1 ) ) = K )
103 1 2 3 4 5 6 7 8 cycpmco2lem2 
 |-  ( ph -> ( U ` E ) = I )
104 103 adantr 
 |-  ( ( ph /\ ( # ` W ) = E ) -> ( U ` E ) = I )
105 89 102 104 3eqtr3d 
 |-  ( ( ph /\ ( # ` W ) = E ) -> K = I )
106 5 eldifbd 
 |-  ( ph -> -. I e. ran W )
107 106 adantr 
 |-  ( ( ph /\ ( # ` W ) = E ) -> -. I e. ran W )
108 105 107 eqneltrd 
 |-  ( ( ph /\ ( # ` W ) = E ) -> -. K e. ran W )
109 11 108 pm2.21dd 
 |-  ( ( ph /\ ( # ` W ) = E ) -> ( ( M ` U ) ` ( U ` ( ( # ` U ) - 1 ) ) ) = ( ( M ` W ) ` ( U ` ( ( # ` U ) - 1 ) ) ) )
110 splcl 
 |-  ( ( W e. Word D /\ <" I "> e. Word D ) -> ( W splice <. E , E , <" I "> >. ) e. Word D )
111 26 15 110 syl2anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) e. Word D )
112 8 111 eqeltrid 
 |-  ( ph -> U e. Word D )
113 nn0p1gt0 
 |-  ( ( # ` W ) e. NN0 -> 0 < ( ( # ` W ) + 1 ) )
114 60 113 syl 
 |-  ( ph -> 0 < ( ( # ` W ) + 1 ) )
115 114 82 breqtrrd 
 |-  ( ph -> 0 < ( # ` U ) )
116 eqidd 
 |-  ( ph -> ( ( # ` U ) - 1 ) = ( ( # ` U ) - 1 ) )
117 1 3 112 91 115 116 cycpmfv2 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( ( # ` U ) - 1 ) ) ) = ( U ` 0 ) )
118 117 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( M ` U ) ` ( U ` ( ( # ` U ) - 1 ) ) ) = ( U ` 0 ) )
119 f1f 
 |-  ( W : dom W -1-1-> D -> W : dom W --> D )
120 43 119 syl 
 |-  ( ph -> W : dom W --> D )
121 120 frnd 
 |-  ( ph -> ran W C_ D )
122 3 121 ssexd 
 |-  ( ph -> ran W e. _V )
123 6 ne0d 
 |-  ( ph -> ran W =/= (/) )
124 hashgt0 
 |-  ( ( ran W e. _V /\ ran W =/= (/) ) -> 0 < ( # ` ran W ) )
125 122 123 124 syl2anc 
 |-  ( ph -> 0 < ( # ` ran W ) )
126 4 dmexd 
 |-  ( ph -> dom W e. _V )
127 hashf1rn 
 |-  ( ( dom W e. _V /\ W : dom W -1-1-> D ) -> ( # ` W ) = ( # ` ran W ) )
128 126 43 127 syl2anc 
 |-  ( ph -> ( # ` W ) = ( # ` ran W ) )
129 125 128 breqtrrd 
 |-  ( ph -> 0 < ( # ` W ) )
130 eqidd 
 |-  ( ph -> ( ( # ` W ) - 1 ) = ( ( # ` W ) - 1 ) )
131 1 3 26 43 129 130 cycpmfv2 
 |-  ( ph -> ( ( M ` W ) ` ( W ` ( ( # ` W ) - 1 ) ) ) = ( W ` 0 ) )
132 131 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( M ` W ) ` ( W ` ( ( # ` W ) - 1 ) ) ) = ( W ` 0 ) )
133 8 a1i 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> U = ( W splice <. E , E , <" I "> >. ) )
134 1 2 3 4 5 6 7 8 cycpmco2lem3 
 |-  ( ph -> ( ( # ` U ) - 1 ) = ( # ` W ) )
135 73 75 addcomd 
 |-  ( ph -> ( E + 1 ) = ( 1 + E ) )
136 135 oveq2d 
 |-  ( ph -> ( ( ( ( # ` W ) - 1 ) - E ) + ( E + 1 ) ) = ( ( ( ( # ` W ) - 1 ) - E ) + ( 1 + E ) ) )
137 72 75 subcld 
 |-  ( ph -> ( ( # ` W ) - 1 ) e. CC )
138 137 73 75 nppcan3d 
 |-  ( ph -> ( ( ( ( # ` W ) - 1 ) - E ) + ( 1 + E ) ) = ( ( ( # ` W ) - 1 ) + 1 ) )
139 72 75 npcand 
 |-  ( ph -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
140 136 138 139 3eqtrd 
 |-  ( ph -> ( ( ( ( # ` W ) - 1 ) - E ) + ( E + 1 ) ) = ( # ` W ) )
141 134 140 eqtr4d 
 |-  ( ph -> ( ( # ` U ) - 1 ) = ( ( ( ( # ` W ) - 1 ) - E ) + ( E + 1 ) ) )
142 141 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( # ` U ) - 1 ) = ( ( ( ( # ` W ) - 1 ) - E ) + ( E + 1 ) ) )
143 133 142 fveq12d 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( U ` ( ( # ` U ) - 1 ) ) = ( ( W splice <. E , E , <" I "> >. ) ` ( ( ( ( # ` W ) - 1 ) - E ) + ( E + 1 ) ) ) )
144 26 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> W e. Word D )
145 nn0fz0 
 |-  ( E e. NN0 <-> E e. ( 0 ... E ) )
146 68 145 sylib 
 |-  ( ph -> E e. ( 0 ... E ) )
147 146 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> E e. ( 0 ... E ) )
148 54 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> E e. ( 0 ... ( # ` W ) ) )
149 15 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> <" I "> e. Word D )
150 72 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( # ` W ) e. CC )
151 1cnd 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> 1 e. CC )
152 73 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> E e. CC )
153 150 151 152 sub32d 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( ( # ` W ) - 1 ) - E ) = ( ( ( # ` W ) - E ) - 1 ) )
154 fznn0sub 
 |-  ( E e. ( 0 ... ( # ` W ) ) -> ( ( # ` W ) - E ) e. NN0 )
155 54 154 syl 
 |-  ( ph -> ( ( # ` W ) - E ) e. NN0 )
156 155 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( # ` W ) - E ) e. NN0 )
157 simpr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( # ` W ) =/= E )
158 150 152 156 157 subne0nn 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( # ` W ) - E ) e. NN )
159 fzo0end 
 |-  ( ( ( # ` W ) - E ) e. NN -> ( ( ( # ` W ) - E ) - 1 ) e. ( 0 ..^ ( ( # ` W ) - E ) ) )
160 158 159 syl 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( ( # ` W ) - E ) - 1 ) e. ( 0 ..^ ( ( # ` W ) - E ) ) )
161 153 160 eqeltrd 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( ( # ` W ) - 1 ) - E ) e. ( 0 ..^ ( ( # ` W ) - E ) ) )
162 s1len 
 |-  ( # ` <" I "> ) = 1
163 162 eqcomi 
 |-  1 = ( # ` <" I "> )
164 163 oveq2i 
 |-  ( E + 1 ) = ( E + ( # ` <" I "> ) )
165 164 a1i 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( E + 1 ) = ( E + ( # ` <" I "> ) ) )
166 144 147 148 149 161 165 splfv3 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( W splice <. E , E , <" I "> >. ) ` ( ( ( ( # ` W ) - 1 ) - E ) + ( E + 1 ) ) ) = ( W ` ( ( ( ( # ` W ) - 1 ) - E ) + E ) ) )
167 137 73 npcand 
 |-  ( ph -> ( ( ( ( # ` W ) - 1 ) - E ) + E ) = ( ( # ` W ) - 1 ) )
168 167 fveq2d 
 |-  ( ph -> ( W ` ( ( ( ( # ` W ) - 1 ) - E ) + E ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
169 168 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( W ` ( ( ( ( # ` W ) - 1 ) - E ) + E ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
170 143 166 169 3eqtrd 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( U ` ( ( # ` U ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
171 170 fveq2d 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( M ` W ) ` ( U ` ( ( # ` U ) - 1 ) ) ) = ( ( M ` W ) ` ( W ` ( ( # ` W ) - 1 ) ) ) )
172 18 fveq1d 
 |-  ( ph -> ( U ` 0 ) = ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) )
173 nn0p1nn 
 |-  ( E e. NN0 -> ( E + 1 ) e. NN )
174 68 173 syl 
 |-  ( ph -> ( E + 1 ) e. NN )
175 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( E + 1 ) ) <-> ( E + 1 ) e. NN )
176 174 175 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ ( E + 1 ) ) )
177 58 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) = ( 0 ..^ ( E + 1 ) ) )
178 176 177 eleqtrrd 
 |-  ( ph -> 0 e. ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) )
179 ccatval1 
 |-  ( ( ( ( W prefix E ) ++ <" I "> ) e. Word D /\ ( W substr <. E , ( # ` W ) >. ) e. Word D /\ 0 e. ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) ) -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) = ( ( ( W prefix E ) ++ <" I "> ) ` 0 ) )
180 30 32 178 179 syl3anc 
 |-  ( ph -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) = ( ( ( W prefix E ) ++ <" I "> ) ` 0 ) )
181 elfzonn0 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( `' W ` J ) e. NN0 )
182 51 181 syl 
 |-  ( ph -> ( `' W ` J ) e. NN0 )
183 nn0p1nn 
 |-  ( ( `' W ` J ) e. NN0 -> ( ( `' W ` J ) + 1 ) e. NN )
184 182 183 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. NN )
185 7 184 eqeltrid 
 |-  ( ph -> E e. NN )
186 lbfzo0 
 |-  ( 0 e. ( 0 ..^ E ) <-> E e. NN )
187 185 186 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ E ) )
188 56 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( W prefix E ) ) ) = ( 0 ..^ E ) )
189 187 188 eleqtrrd 
 |-  ( ph -> 0 e. ( 0 ..^ ( # ` ( W prefix E ) ) ) )
190 ccatval1 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D /\ 0 e. ( 0 ..^ ( # ` ( W prefix E ) ) ) ) -> ( ( ( W prefix E ) ++ <" I "> ) ` 0 ) = ( ( W prefix E ) ` 0 ) )
191 28 15 189 190 syl3anc 
 |-  ( ph -> ( ( ( W prefix E ) ++ <" I "> ) ` 0 ) = ( ( W prefix E ) ` 0 ) )
192 nn0p1gt0 
 |-  ( ( `' W ` J ) e. NN0 -> 0 < ( ( `' W ` J ) + 1 ) )
193 182 192 syl 
 |-  ( ph -> 0 < ( ( `' W ` J ) + 1 ) )
194 193 7 breqtrrdi 
 |-  ( ph -> 0 < E )
195 194 gt0ne0d 
 |-  ( ph -> E =/= 0 )
196 fzne1 
 |-  ( ( E e. ( 0 ... ( # ` W ) ) /\ E =/= 0 ) -> E e. ( ( 0 + 1 ) ... ( # ` W ) ) )
197 54 195 196 syl2anc 
 |-  ( ph -> E e. ( ( 0 + 1 ) ... ( # ` W ) ) )
198 0p1e1 
 |-  ( 0 + 1 ) = 1
199 198 oveq1i 
 |-  ( ( 0 + 1 ) ... ( # ` W ) ) = ( 1 ... ( # ` W ) )
200 197 199 eleqtrdi 
 |-  ( ph -> E e. ( 1 ... ( # ` W ) ) )
201 pfxfv0 
 |-  ( ( W e. Word D /\ E e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix E ) ` 0 ) = ( W ` 0 ) )
202 26 200 201 syl2anc 
 |-  ( ph -> ( ( W prefix E ) ` 0 ) = ( W ` 0 ) )
203 180 191 202 3eqtrd 
 |-  ( ph -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) = ( W ` 0 ) )
204 172 203 eqtrd 
 |-  ( ph -> ( U ` 0 ) = ( W ` 0 ) )
205 204 adantr 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( U ` 0 ) = ( W ` 0 ) )
206 132 171 205 3eqtr4rd 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( U ` 0 ) = ( ( M ` W ) ` ( U ` ( ( # ` U ) - 1 ) ) ) )
207 118 206 eqtrd 
 |-  ( ( ph /\ ( # ` W ) =/= E ) -> ( ( M ` U ) ` ( U ` ( ( # ` U ) - 1 ) ) ) = ( ( M ` W ) ` ( U ` ( ( # ` U ) - 1 ) ) ) )
208 109 207 pm2.61dane 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( ( # ` U ) - 1 ) ) ) = ( ( M ` W ) ` ( U ` ( ( # ` U ) - 1 ) ) ) )
209 101 fveq2d 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( ( # ` U ) - 1 ) ) ) = ( ( M ` U ) ` K ) )
210 101 fveq2d 
 |-  ( ph -> ( ( M ` W ) ` ( U ` ( ( # ` U ) - 1 ) ) ) = ( ( M ` W ) ` K ) )
211 208 209 210 3eqtr3d 
 |-  ( ph -> ( ( M ` U ) ` K ) = ( ( M ` W ) ` K ) )