Theorem cycpmco2lem4

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 "> >. )
Assertion	cycpmco2lem4	|- ( ph -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` I ) ) = ( ( M ` U ) ` I ) )

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	1 2 3 4 5 6 7 8	cycpmco2lem1	|- ( ph -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` I ) ) = ( ( M ` W ) ` J ) )
10	3	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> D e. V )
11		ssrab2	|- { w e. Word D | w : dom w -1-1-> D } C_ Word D
12		eqid	|- ( Base ` S ) = ( Base ` S )
13	1 2 12	tocycf	|- ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
14	3 13	syl	|- ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
15	14	fdmd	|- ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
16	4 15	eleqtrd	|- ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
17	11 16	sselid	|- ( ph -> W e. Word D )
18	5	eldifad	|- ( ph -> I e. D )
19	18	s1cld	|- ( ph -> <" I "> e. Word D )
20		splcl	|- ( ( W e. Word D /\ <" I "> e. Word D ) -> ( W splice <. E , E , <" I "> >. ) e. Word D )
21	17 19 20	syl2anc	|- ( ph -> ( W splice <. E , E , <" I "> >. ) e. Word D )
22	8 21	eqeltrid	|- ( ph -> U e. Word D )
23	22	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> U e. Word D )
24	1 2 3 4 5 6 7 8	cycpmco2f1	|- ( ph -> U : dom U -1-1-> D )
25	24	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> U : dom U -1-1-> D )
26		simpr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> E e. ( 0 ..^ ( # ` W ) ) )
27	1 2 3 4 5 6 7 8	cycpmco2lem3	|- ( ph -> ( ( # ` U ) - 1 ) = ( # ` W ) )
28	27	oveq2d	|- ( ph -> ( 0 ..^ ( ( # ` U ) - 1 ) ) = ( 0 ..^ ( # ` W ) ) )
29	28	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( ( # ` U ) - 1 ) ) = ( 0 ..^ ( # ` W ) ) )
30	26 29	eleqtrrd	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> E e. ( 0 ..^ ( ( # ` U ) - 1 ) ) )
31	1 10 23 25 30	cycpmfv1	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( M ` U ) ` ( U ` E ) ) = ( U ` ( E + 1 ) ) )
32	1 2 3 4 5 6 7 8	cycpmco2lem2	|- ( ph -> ( U ` E ) = I )
33	32	fveq2d	|- ( ph -> ( ( M ` U ) ` ( U ` E ) ) = ( ( M ` U ) ` I ) )
34	33	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( M ` U ) ` ( U ` E ) ) = ( ( M ` U ) ` I ) )
35	17	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> W e. Word D )
36		lencl	|- ( W e. Word D -> ( # ` W ) e. NN0 )
37	17 36	syl	|- ( ph -> ( # ` W ) e. NN0 )
38		nn0fz0	|- ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
39	37 38	sylib	|- ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
40	39	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
41		swrdfv0	|- ( ( W e. Word D /\ E e. ( 0 ..^ ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( ( W substr <. E , ( # ` W ) >. ) ` 0 ) = ( W ` E ) )
42	35 26 40 41	syl3anc	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W substr <. E , ( # ` W ) >. ) ` 0 ) = ( W ` E ) )
43		ovexd	|- ( ph -> ( ( `' W ` J ) + 1 ) e. _V )
44	7 43	eqeltrid	|- ( ph -> E e. _V )
45		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 ) >. ) ) )
46	4 44 44 19 45	syl13anc	|- ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
47	8 46	syl5eq	|- ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
48	47	fveq1d	|- ( ph -> ( U ` ( E + 1 ) ) = ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` ( E + 1 ) ) )
49	48	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( U ` ( E + 1 ) ) = ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` ( E + 1 ) ) )
50		pfxcl	|- ( W e. Word D -> ( W prefix E ) e. Word D )
51	17 50	syl	|- ( ph -> ( W prefix E ) e. Word D )
52		ccatcl	|- ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
53	51 19 52	syl2anc	|- ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
54	53	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
55		swrdcl	|- ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
56	17 55	syl	|- ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
57	56	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
58		1z	|- 1 e. ZZ
59		fzoaddel	|- ( ( E e. ( 0 ..^ ( # ` W ) ) /\ 1 e. ZZ ) -> ( E + 1 ) e. ( ( 0 + 1 ) ..^ ( ( # ` W ) + 1 ) ) )
60	58 59	mpan2	|- ( E e. ( 0 ..^ ( # ` W ) ) -> ( E + 1 ) e. ( ( 0 + 1 ) ..^ ( ( # ` W ) + 1 ) ) )
61		elfzolt2b	|- ( ( E + 1 ) e. ( ( 0 + 1 ) ..^ ( ( # ` W ) + 1 ) ) -> ( E + 1 ) e. ( ( E + 1 ) ..^ ( ( # ` W ) + 1 ) ) )
62	60 61	syl	|- ( E e. ( 0 ..^ ( # ` W ) ) -> ( E + 1 ) e. ( ( E + 1 ) ..^ ( ( # ` W ) + 1 ) ) )
63	62	adantl	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( E + 1 ) e. ( ( E + 1 ) ..^ ( ( # ` W ) + 1 ) ) )
64		ccatws1len	|- ( ( W prefix E ) e. Word D -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
65	51 64	syl	|- ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
66		id	|- ( w = W -> w = W )
67		dmeq	|- ( w = W -> dom w = dom W )
68		eqidd	|- ( w = W -> D = D )
69	66 67 68	f1eq123d	|- ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
70	69	elrab3	|- ( W e. Word D -> ( W e. { w e. Word D | w : dom w -1-1-> D } <-> W : dom W -1-1-> D ) )
71	70	biimpa	|- ( ( W e. Word D /\ W e. { w e. Word D | w : dom w -1-1-> D } ) -> W : dom W -1-1-> D )
72	17 16 71	syl2anc	|- ( ph -> W : dom W -1-1-> D )
73		f1cnv	|- ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
74	72 73	syl	|- ( ph -> `' W : ran W -1-1-onto-> dom W )
75		f1of	|- ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
76	74 75	syl	|- ( ph -> `' W : ran W --> dom W )
77	76 6	ffvelrnd	|- ( ph -> ( `' W ` J ) e. dom W )
78		wrddm	|- ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
79	17 78	syl	|- ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
80	77 79	eleqtrd	|- ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
81		fzofzp1	|- ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
82	80 81	syl	|- ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
83	7 82	eqeltrid	|- ( ph -> E e. ( 0 ... ( # ` W ) ) )
84		pfxlen	|- ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix E ) ) = E )
85	17 83 84	syl2anc	|- ( ph -> ( # ` ( W prefix E ) ) = E )
86	85	oveq1d	|- ( ph -> ( ( # ` ( W prefix E ) ) + 1 ) = ( E + 1 ) )
87	65 86	eqtrd	|- ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( E + 1 ) )
88	87	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( E + 1 ) )
89	47	fveq2d	|- ( ph -> ( # ` U ) = ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) )
90		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 ) >. ) ) ) )
91	53 56 90	syl2anc	|- ( ph -> ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) )
92		swrdlen	|- ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
93	17 83 39 92	syl3anc	|- ( ph -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
94	87 93	oveq12d	|- ( ph -> ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
95	89 91 94	3eqtrd	|- ( ph -> ( # ` U ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
96		fz0ssnn0	|- ( 0 ... ( # ` W ) ) C_ NN0
97	96 83	sselid	|- ( ph -> E e. NN0 )
98	97	nn0zd	|- ( ph -> E e. ZZ )
99	98	peano2zd	|- ( ph -> ( E + 1 ) e. ZZ )
100	99	zcnd	|- ( ph -> ( E + 1 ) e. CC )
101	37	nn0cnd	|- ( ph -> ( # ` W ) e. CC )
102	97	nn0cnd	|- ( ph -> E e. CC )
103	100 101 102	addsubassd	|- ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
104		1cnd	|- ( ph -> 1 e. CC )
105	102 104 101	addassd	|- ( ph -> ( ( E + 1 ) + ( # ` W ) ) = ( E + ( 1 + ( # ` W ) ) ) )
106	105	oveq1d	|- ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
107	95 103 106	3eqtr2d	|- ( ph -> ( # ` U ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
108	104 101	addcld	|- ( ph -> ( 1 + ( # ` W ) ) e. CC )
109	102 108	pncan2d	|- ( ph -> ( ( E + ( 1 + ( # ` W ) ) ) - E ) = ( 1 + ( # ` W ) ) )
110	104 101	addcomd	|- ( ph -> ( 1 + ( # ` W ) ) = ( ( # ` W ) + 1 ) )
111	107 109 110	3eqtrd	|- ( ph -> ( # ` U ) = ( ( # ` W ) + 1 ) )
112	89 111 91	3eqtr3rd	|- ( ph -> ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` W ) + 1 ) )
113	112	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` W ) + 1 ) )
114	88 113	oveq12d	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) ..^ ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) ) = ( ( E + 1 ) ..^ ( ( # ` W ) + 1 ) ) )
115	63 114	eleqtrrd	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( E + 1 ) e. ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) ..^ ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) ) )
116		ccatval2	|- ( ( ( ( W prefix E ) ++ <" I "> ) e. Word D /\ ( W substr <. E , ( # ` W ) >. ) e. Word D /\ ( E + 1 ) e. ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) ..^ ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) ) ) -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` ( E + 1 ) ) = ( ( W substr <. E , ( # ` W ) >. ) ` ( ( E + 1 ) - ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) ) )
117	54 57 115 116	syl3anc	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` ( E + 1 ) ) = ( ( W substr <. E , ( # ` W ) >. ) ` ( ( E + 1 ) - ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) ) )
118	87	oveq2d	|- ( ph -> ( ( E + 1 ) - ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) = ( ( E + 1 ) - ( E + 1 ) ) )
119	100	subidd	|- ( ph -> ( ( E + 1 ) - ( E + 1 ) ) = 0 )
120	118 119	eqtrd	|- ( ph -> ( ( E + 1 ) - ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) = 0 )
121	120	fveq2d	|- ( ph -> ( ( W substr <. E , ( # ` W ) >. ) ` ( ( E + 1 ) - ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) ) = ( ( W substr <. E , ( # ` W ) >. ) ` 0 ) )
122	121	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W substr <. E , ( # ` W ) >. ) ` ( ( E + 1 ) - ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) ) = ( ( W substr <. E , ( # ` W ) >. ) ` 0 ) )
123	49 117 122	3eqtrd	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( U ` ( E + 1 ) ) = ( ( W substr <. E , ( # ` W ) >. ) ` 0 ) )
124	7	fveq2i	|- ( W ` E ) = ( W ` ( ( `' W ` J ) + 1 ) )
125	124	a1i	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` E ) = ( W ` ( ( `' W ` J ) + 1 ) ) )
126	72	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> W : dom W -1-1-> D )
127	7	oveq1i	|- ( E - 1 ) = ( ( ( `' W ` J ) + 1 ) - 1 )
128		elfzonn0	|- ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( `' W ` J ) e. NN0 )
129	80 128	syl	|- ( ph -> ( `' W ` J ) e. NN0 )
130	129	nn0cnd	|- ( ph -> ( `' W ` J ) e. CC )
131	130 104	pncand	|- ( ph -> ( ( ( `' W ` J ) + 1 ) - 1 ) = ( `' W ` J ) )
132	127 131	eqtr2id	|- ( ph -> ( `' W ` J ) = ( E - 1 ) )
133	132	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( `' W ` J ) = ( E - 1 ) )
134		nn0p1gt0	|- ( ( `' W ` J ) e. NN0 -> 0 < ( ( `' W ` J ) + 1 ) )
135	129 134	syl	|- ( ph -> 0 < ( ( `' W ` J ) + 1 ) )
136	135 7	breqtrrdi	|- ( ph -> 0 < E )
137	136	gt0ne0d	|- ( ph -> E =/= 0 )
138	137	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> E =/= 0 )
139		fzo1fzo0n0	|- ( E e. ( 1 ..^ ( # ` W ) ) <-> ( E e. ( 0 ..^ ( # ` W ) ) /\ E =/= 0 ) )
140	26 138 139	sylanbrc	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> E e. ( 1 ..^ ( # ` W ) ) )
141		elfzo1elm1fzo0	|- ( E e. ( 1 ..^ ( # ` W ) ) -> ( E - 1 ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
142	140 141	syl	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( E - 1 ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
143	133 142	eqeltrd	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( `' W ` J ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
144	1 10 35 126 143	cycpmfv1	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( M ` W ) ` ( W ` ( `' W ` J ) ) ) = ( W ` ( ( `' W ` J ) + 1 ) ) )
145		f1f1orn	|- ( W : dom W -1-1-> D -> W : dom W -1-1-onto-> ran W )
146	72 145	syl	|- ( ph -> W : dom W -1-1-onto-> ran W )
147		f1ocnvfv2	|- ( ( W : dom W -1-1-onto-> ran W /\ J e. ran W ) -> ( W ` ( `' W ` J ) ) = J )
148	146 6 147	syl2anc	|- ( ph -> ( W ` ( `' W ` J ) ) = J )
149	148	fveq2d	|- ( ph -> ( ( M ` W ) ` ( W ` ( `' W ` J ) ) ) = ( ( M ` W ) ` J ) )
150	149	adantr	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( M ` W ) ` ( W ` ( `' W ` J ) ) ) = ( ( M ` W ) ` J ) )
151	125 144 150	3eqtr2rd	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( M ` W ) ` J ) = ( W ` E ) )
152	42 123 151	3eqtr4d	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( U ` ( E + 1 ) ) = ( ( M ` W ) ` J ) )
153	31 34 152	3eqtr3rd	|- ( ( ph /\ E e. ( 0 ..^ ( # ` W ) ) ) -> ( ( M ` W ) ` J ) = ( ( M ` U ) ` I ) )
154	149	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( M ` W ) ` ( W ` ( `' W ` J ) ) ) = ( ( M ` W ) ` J ) )
155	3	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> D e. V )
156	17	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> W e. Word D )
157	72	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> W : dom W -1-1-> D )
158	136	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> 0 < E )
159		simpr	|- ( ( ph /\ E = ( # ` W ) ) -> E = ( # ` W ) )
160	158 159	breqtrd	|- ( ( ph /\ E = ( # ` W ) ) -> 0 < ( # ` W ) )
161		oveq1	|- ( E = ( # ` W ) -> ( E - 1 ) = ( ( # ` W ) - 1 ) )
162	132 161	sylan9eq	|- ( ( ph /\ E = ( # ` W ) ) -> ( `' W ` J ) = ( ( # ` W ) - 1 ) )
163	1 155 156 157 160 162	cycpmfv2	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( M ` W ) ` ( W ` ( `' W ` J ) ) ) = ( W ` 0 ) )
164	154 163	eqtr3d	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( M ` W ) ` J ) = ( W ` 0 ) )
165	22	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> U e. Word D )
166	24	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> U : dom U -1-1-> D )
167		nn0p1gt0	|- ( ( # ` W ) e. NN0 -> 0 < ( ( # ` W ) + 1 ) )
168	37 167	syl	|- ( ph -> 0 < ( ( # ` W ) + 1 ) )
169	168 111	breqtrrd	|- ( ph -> 0 < ( # ` U ) )
170	169	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> 0 < ( # ` U ) )
171	27	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( # ` U ) - 1 ) = ( # ` W ) )
172	159 171	eqtr4d	|- ( ( ph /\ E = ( # ` W ) ) -> E = ( ( # ` U ) - 1 ) )
173	1 155 165 166 170 172	cycpmfv2	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( M ` U ) ` ( U ` E ) ) = ( U ` 0 ) )
174	47	fveq1d	|- ( ph -> ( U ` 0 ) = ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) )
175	174	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> ( U ` 0 ) = ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) )
176		nn0p1nn	|- ( E e. NN0 -> ( E + 1 ) e. NN )
177	97 176	syl	|- ( ph -> ( E + 1 ) e. NN )
178		lbfzo0	|- ( 0 e. ( 0 ..^ ( E + 1 ) ) <-> ( E + 1 ) e. NN )
179	177 178	sylibr	|- ( ph -> 0 e. ( 0 ..^ ( E + 1 ) ) )
180	87	oveq2d	|- ( ph -> ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) = ( 0 ..^ ( E + 1 ) ) )
181	179 180	eleqtrrd	|- ( ph -> 0 e. ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) )
182		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 ) )
183	53 56 181 182	syl3anc	|- ( ph -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) = ( ( ( W prefix E ) ++ <" I "> ) ` 0 ) )
184		nn0p1nn	|- ( ( `' W ` J ) e. NN0 -> ( ( `' W ` J ) + 1 ) e. NN )
185	129 184	syl	|- ( ph -> ( ( `' W ` J ) + 1 ) e. NN )
186	7 185	eqeltrid	|- ( ph -> E e. NN )
187		lbfzo0	|- ( 0 e. ( 0 ..^ E ) <-> E e. NN )
188	186 187	sylibr	|- ( ph -> 0 e. ( 0 ..^ E ) )
189	85	oveq2d	|- ( ph -> ( 0 ..^ ( # ` ( W prefix E ) ) ) = ( 0 ..^ E ) )
190	188 189	eleqtrrd	|- ( ph -> 0 e. ( 0 ..^ ( # ` ( W prefix E ) ) ) )
191		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 ) )
192	51 19 190 191	syl3anc	|- ( ph -> ( ( ( W prefix E ) ++ <" I "> ) ` 0 ) = ( ( W prefix E ) ` 0 ) )
193		fzne1	|- ( ( E e. ( 0 ... ( # ` W ) ) /\ E =/= 0 ) -> E e. ( ( 0 + 1 ) ... ( # ` W ) ) )
194	83 137 193	syl2anc	|- ( ph -> E e. ( ( 0 + 1 ) ... ( # ` W ) ) )
195		0p1e1	|- ( 0 + 1 ) = 1
196	195	oveq1i	|- ( ( 0 + 1 ) ... ( # ` W ) ) = ( 1 ... ( # ` W ) )
197	194 196	eleqtrdi	|- ( ph -> E e. ( 1 ... ( # ` W ) ) )
198		pfxfv0	|- ( ( W e. Word D /\ E e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix E ) ` 0 ) = ( W ` 0 ) )
199	17 197 198	syl2anc	|- ( ph -> ( ( W prefix E ) ` 0 ) = ( W ` 0 ) )
200	183 192 199	3eqtrd	|- ( ph -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) = ( W ` 0 ) )
201	200	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` 0 ) = ( W ` 0 ) )
202	173 175 201	3eqtrd	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( M ` U ) ` ( U ` E ) ) = ( W ` 0 ) )
203	33	adantr	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( M ` U ) ` ( U ` E ) ) = ( ( M ` U ) ` I ) )
204	164 202 203	3eqtr2d	|- ( ( ph /\ E = ( # ` W ) ) -> ( ( M ` W ) ` J ) = ( ( M ` U ) ` I ) )
205		elfzr	|- ( E e. ( 0 ... ( # ` W ) ) -> ( E e. ( 0 ..^ ( # ` W ) ) \/ E = ( # ` W ) ) )
206	83 205	syl	|- ( ph -> ( E e. ( 0 ..^ ( # ` W ) ) \/ E = ( # ` W ) ) )
207	153 204 206	mpjaodan	|- ( ph -> ( ( M ` W ) ` J ) = ( ( M ` U ) ` I ) )
208	9 207	eqtrd	|- ( ph -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` I ) ) = ( ( M ` U ) ` I ) )