Metamath Proof Explorer

Theorem cycpmco2

Description: The composition of a cyclic permutation and a transposition of one element in the cycle and one outside the cycle results in a cyclic permutation with one more element in its orbit. (Contributed by Thierry Arnoux, 2-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 cycpmco2 
|- ( ph -> ( ( M ` W ) o. ( M ` <" I J "> ) ) = ( M ` U ) )

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 eqid 
 |-  ( Base ` S ) = ( Base ` S )
10 1 2 9 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
11 3 10 syl 
 |-  ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
12 11 fdmd 
 |-  ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
13 4 12 eleqtrd 
 |-  ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
14 11 13 ffvelrnd 
 |-  ( ph -> ( M ` W ) e. ( Base ` S ) )
15 2 9 symgbasf 
 |-  ( ( M ` W ) e. ( Base ` S ) -> ( M ` W ) : D --> D )
16 14 15 syl 
 |-  ( ph -> ( M ` W ) : D --> D )
17 16 ffnd 
 |-  ( ph -> ( M ` W ) Fn D )
18 5 eldifad 
 |-  ( ph -> I e. D )
19 ssrab2 
 |-  { w e. Word D | w : dom w -1-1-> D } C_ Word D
20 19 13 sselid 
 |-  ( ph -> W e. Word D )
21 id 
 |-  ( w = W -> w = W )
22 dmeq 
 |-  ( w = W -> dom w = dom W )
23 eqidd 
 |-  ( w = W -> D = D )
24 21 22 23 f1eq123d 
 |-  ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
25 24 elrab3 
 |-  ( W e. Word D -> ( W e. { w e. Word D | w : dom w -1-1-> D } <-> W : dom W -1-1-> D ) )
26 25 biimpa 
 |-  ( ( W e. Word D /\ W e. { w e. Word D | w : dom w -1-1-> D } ) -> W : dom W -1-1-> D )
27 20 13 26 syl2anc 
 |-  ( ph -> W : dom W -1-1-> D )
28 f1f 
 |-  ( W : dom W -1-1-> D -> W : dom W --> D )
29 27 28 syl 
 |-  ( ph -> W : dom W --> D )
30 29 frnd 
 |-  ( ph -> ran W C_ D )
31 30 6 sseldd 
 |-  ( ph -> J e. D )
32 5 eldifbd 
 |-  ( ph -> -. I e. ran W )
33 nelne2 
 |-  ( ( J e. ran W /\ -. I e. ran W ) -> J =/= I )
34 6 32 33 syl2anc 
 |-  ( ph -> J =/= I )
35 34 necomd 
 |-  ( ph -> I =/= J )
36 1 3 18 31 35 2 cycpm2cl 
 |-  ( ph -> ( M ` <" I J "> ) e. ( Base ` S ) )
37 2 9 symgbasf 
 |-  ( ( M ` <" I J "> ) e. ( Base ` S ) -> ( M ` <" I J "> ) : D --> D )
38 36 37 syl 
 |-  ( ph -> ( M ` <" I J "> ) : D --> D )
39 38 ffnd 
 |-  ( ph -> ( M ` <" I J "> ) Fn D )
40 38 frnd 
 |-  ( ph -> ran ( M ` <" I J "> ) C_ D )
41 fnco 
 |-  ( ( ( M ` W ) Fn D /\ ( M ` <" I J "> ) Fn D /\ ran ( M ` <" I J "> ) C_ D ) -> ( ( M ` W ) o. ( M ` <" I J "> ) ) Fn D )
42 17 39 40 41 syl3anc 
 |-  ( ph -> ( ( M ` W ) o. ( M ` <" I J "> ) ) Fn D )
43 18 s1cld 
 |-  ( ph -> <" I "> e. Word D )
44 splcl 
 |-  ( ( W e. Word D /\ <" I "> e. Word D ) -> ( W splice <. E , E , <" I "> >. ) e. Word D )
45 20 43 44 syl2anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) e. Word D )
46 8 45 eqeltrid 
 |-  ( ph -> U e. Word D )
47 1 2 3 4 5 6 7 8 cycpmco2f1 
 |-  ( ph -> U : dom U -1-1-> D )
48 1 3 46 47 2 cycpmcl 
 |-  ( ph -> ( M ` U ) e. ( Base ` S ) )
49 2 9 symgbasf 
 |-  ( ( M ` U ) e. ( Base ` S ) -> ( M ` U ) : D --> D )
50 48 49 syl 
 |-  ( ph -> ( M ` U ) : D --> D )
51 50 ffnd 
 |-  ( ph -> ( M ` U ) Fn D )
52 fvco3 
 |-  ( ( ( M ` <" I J "> ) : D --> D /\ i e. D ) -> ( ( ( M ` W ) o. ( M ` <" I J "> ) ) ` i ) = ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) )
53 38 52 sylan 
 |-  ( ( ph /\ i e. D ) -> ( ( ( M ` W ) o. ( M ` <" I J "> ) ) ` i ) = ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) )
54 1 3 18 31 35 2 cyc2fv2 
 |-  ( ph -> ( ( M ` <" I J "> ) ` J ) = I )
55 54 fveq2d 
 |-  ( ph -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` J ) ) = ( ( M ` W ) ` I ) )
56 1 2 3 4 5 6 7 8 cycpmco2lem2 
 |-  ( ph -> ( U ` E ) = I )
57 f1cnv 
 |-  ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
58 f1of 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
59 27 57 58 3syl 
 |-  ( ph -> `' W : ran W --> dom W )
60 59 6 ffvelrnd 
 |-  ( ph -> ( `' W ` J ) e. dom W )
61 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
62 20 61 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
63 60 62 eleqtrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
64 lencl 
 |-  ( W e. Word D -> ( # ` W ) e. NN0 )
65 20 64 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
66 65 nn0cnd 
 |-  ( ph -> ( # ` W ) e. CC )
67 1cnd 
 |-  ( ph -> 1 e. CC )
68 ovexd 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. _V )
69 7 68 eqeltrid 
 |-  ( ph -> E e. _V )
70 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 ) >. ) ) )
71 4 69 69 43 70 syl13anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
72 8 71 syl5eq 
 |-  ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
73 72 fveq2d 
 |-  ( ph -> ( # ` U ) = ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) )
74 pfxcl 
 |-  ( W e. Word D -> ( W prefix E ) e. Word D )
75 20 74 syl 
 |-  ( ph -> ( W prefix E ) e. Word D )
76 ccatcl 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
77 75 43 76 syl2anc 
 |-  ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
78 swrdcl 
 |-  ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
79 20 78 syl 
 |-  ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
80 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 ) >. ) ) ) )
81 77 79 80 syl2anc 
 |-  ( ph -> ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) )
82 ccatws1len 
 |-  ( ( W prefix E ) e. Word D -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
83 20 74 82 3syl 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
84 fzofzp1 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
85 63 84 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
86 7 85 eqeltrid 
 |-  ( ph -> E e. ( 0 ... ( # ` W ) ) )
87 pfxlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix E ) ) = E )
88 20 86 87 syl2anc 
 |-  ( ph -> ( # ` ( W prefix E ) ) = E )
89 88 oveq1d 
 |-  ( ph -> ( ( # ` ( W prefix E ) ) + 1 ) = ( E + 1 ) )
90 83 89 eqtrd 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( E + 1 ) )
91 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
92 65 91 sylib 
 |-  ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
93 swrdlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
94 20 86 92 93 syl3anc 
 |-  ( ph -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
95 90 94 oveq12d 
 |-  ( ph -> ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
96 73 81 95 3eqtrd 
 |-  ( ph -> ( # ` U ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
97 fz0ssnn0 
 |-  ( 0 ... ( # ` W ) ) C_ NN0
98 97 86 sselid 
 |-  ( ph -> E e. NN0 )
99 98 nn0zd 
 |-  ( ph -> E e. ZZ )
100 99 peano2zd 
 |-  ( ph -> ( E + 1 ) e. ZZ )
101 100 zcnd 
 |-  ( ph -> ( E + 1 ) e. CC )
102 98 nn0cnd 
 |-  ( ph -> E e. CC )
103 101 66 102 addsubassd 
 |-  ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
104 102 67 66 addassd 
 |-  ( ph -> ( ( E + 1 ) + ( # ` W ) ) = ( E + ( 1 + ( # ` W ) ) ) )
105 104 oveq1d 
 |-  ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
106 96 103 105 3eqtr2d 
 |-  ( ph -> ( # ` U ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
107 67 66 addcld 
 |-  ( ph -> ( 1 + ( # ` W ) ) e. CC )
108 102 107 pncan2d 
 |-  ( ph -> ( ( E + ( 1 + ( # ` W ) ) ) - E ) = ( 1 + ( # ` W ) ) )
109 67 66 addcomd 
 |-  ( ph -> ( 1 + ( # ` W ) ) = ( ( # ` W ) + 1 ) )
110 106 108 109 3eqtrd 
 |-  ( ph -> ( # ` U ) = ( ( # ` W ) + 1 ) )
111 66 67 110 mvrraddd 
 |-  ( ph -> ( ( # ` U ) - 1 ) = ( # ` W ) )
112 111 oveq2d 
 |-  ( ph -> ( 0 ..^ ( ( # ` U ) - 1 ) ) = ( 0 ..^ ( # ` W ) ) )
113 63 112 eleqtrrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) )
114 1 3 46 47 113 cycpmfv1 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( `' W ` J ) ) ) = ( U ` ( ( `' W ` J ) + 1 ) ) )
115 7 fveq2i 
 |-  ( U ` E ) = ( U ` ( ( `' W ` J ) + 1 ) )
116 114 115 eqtr4di 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( `' W ` J ) ) ) = ( U ` E ) )
117 1 3 20 27 18 32 cycpmfv3 
 |-  ( ph -> ( ( M ` W ) ` I ) = I )
118 56 116 117 3eqtr4d 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( `' W ` J ) ) ) = ( ( M ` W ) ` I ) )
119 72 fveq1d 
 |-  ( ph -> ( U ` ( `' W ` J ) ) = ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` ( `' W ` J ) ) )
120 fzossfzop1 
 |-  ( E e. NN0 -> ( 0 ..^ E ) C_ ( 0 ..^ ( E + 1 ) ) )
121 98 120 syl 
 |-  ( ph -> ( 0 ..^ E ) C_ ( 0 ..^ ( E + 1 ) ) )
122 elfzonn0 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( `' W ` J ) e. NN0 )
123 fzonn0p1 
 |-  ( ( `' W ` J ) e. NN0 -> ( `' W ` J ) e. ( 0 ..^ ( ( `' W ` J ) + 1 ) ) )
124 63 122 123 3syl 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( ( `' W ` J ) + 1 ) ) )
125 7 oveq2i 
 |-  ( 0 ..^ E ) = ( 0 ..^ ( ( `' W ` J ) + 1 ) )
126 124 125 eleqtrrdi 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ E ) )
127 121 126 sseldd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( E + 1 ) ) )
128 90 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) = ( 0 ..^ ( E + 1 ) ) )
129 127 128 eleqtrrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) )
130 ccatval1 
 |-  ( ( ( ( W prefix E ) ++ <" I "> ) e. Word D /\ ( W substr <. E , ( # ` W ) >. ) e. Word D /\ ( `' W ` J ) e. ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) ) -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` ( `' W ` J ) ) = ( ( ( W prefix E ) ++ <" I "> ) ` ( `' W ` J ) ) )
131 77 79 129 130 syl3anc 
 |-  ( ph -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` ( `' W ` J ) ) = ( ( ( W prefix E ) ++ <" I "> ) ` ( `' W ` J ) ) )
132 88 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( W prefix E ) ) ) = ( 0 ..^ E ) )
133 126 132 eleqtrrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` ( W prefix E ) ) ) )
134 ccatval1 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D /\ ( `' W ` J ) e. ( 0 ..^ ( # ` ( W prefix E ) ) ) ) -> ( ( ( W prefix E ) ++ <" I "> ) ` ( `' W ` J ) ) = ( ( W prefix E ) ` ( `' W ` J ) ) )
135 75 43 133 134 syl3anc 
 |-  ( ph -> ( ( ( W prefix E ) ++ <" I "> ) ` ( `' W ` J ) ) = ( ( W prefix E ) ` ( `' W ` J ) ) )
136 119 131 135 3eqtrd 
 |-  ( ph -> ( U ` ( `' W ` J ) ) = ( ( W prefix E ) ` ( `' W ` J ) ) )
137 pfxfv 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( `' W ` J ) e. ( 0 ..^ E ) ) -> ( ( W prefix E ) ` ( `' W ` J ) ) = ( W ` ( `' W ` J ) ) )
138 20 86 126 137 syl3anc 
 |-  ( ph -> ( ( W prefix E ) ` ( `' W ` J ) ) = ( W ` ( `' W ` J ) ) )
139 f1f1orn 
 |-  ( W : dom W -1-1-> D -> W : dom W -1-1-onto-> ran W )
140 27 139 syl 
 |-  ( ph -> W : dom W -1-1-onto-> ran W )
141 f1ocnvfv2 
 |-  ( ( W : dom W -1-1-onto-> ran W /\ J e. ran W ) -> ( W ` ( `' W ` J ) ) = J )
142 140 6 141 syl2anc 
 |-  ( ph -> ( W ` ( `' W ` J ) ) = J )
143 136 138 142 3eqtrd 
 |-  ( ph -> ( U ` ( `' W ` J ) ) = J )
144 143 fveq2d 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( `' W ` J ) ) ) = ( ( M ` U ) ` J ) )
145 55 118 144 3eqtr2d 
 |-  ( ph -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` J ) ) = ( ( M ` U ) ` J ) )
146 145 ad2antrr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i = J ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` J ) ) = ( ( M ` U ) ` J ) )
147 simpr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i = J ) -> i = J )
148 147 fveq2d 
 |-  ( ( ( ph /\ i e. ran W ) /\ i = J ) -> ( ( M ` <" I J "> ) ` i ) = ( ( M ` <" I J "> ) ` J ) )
149 148 fveq2d 
 |-  ( ( ( ph /\ i e. ran W ) /\ i = J ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` W ) ` ( ( M ` <" I J "> ) ` J ) ) )
150 147 fveq2d 
 |-  ( ( ( ph /\ i e. ran W ) /\ i = J ) -> ( ( M ` U ) ` i ) = ( ( M ` U ) ` J ) )
151 146 149 150 3eqtr4d 
 |-  ( ( ( ph /\ i e. ran W ) /\ i = J ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
152 3 ad2antrr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> D e. V )
153 18 31 s2cld 
 |-  ( ph -> <" I J "> e. Word D )
154 153 ad2antrr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> <" I J "> e. Word D )
155 18 31 35 s2f1 
 |-  ( ph -> <" I J "> : dom <" I J "> -1-1-> D )
156 155 ad2antrr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> <" I J "> : dom <" I J "> -1-1-> D )
157 30 sselda 
 |-  ( ( ph /\ i e. ran W ) -> i e. D )
158 157 adantr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> i e. D )
159 simpr 
 |-  ( ( ph /\ i e. ran W ) -> i e. ran W )
160 32 adantr 
 |-  ( ( ph /\ i e. ran W ) -> -. I e. ran W )
161 nelne2 
 |-  ( ( i e. ran W /\ -. I e. ran W ) -> i =/= I )
162 159 160 161 syl2anc 
 |-  ( ( ph /\ i e. ran W ) -> i =/= I )
163 162 adantr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> i =/= I )
164 simpr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> i =/= J )
165 163 164 nelprd 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> -. i e. { I , J } )
166 18 31 s2rn 
 |-  ( ph -> ran <" I J "> = { I , J } )
167 166 eleq2d 
 |-  ( ph -> ( i e. ran <" I J "> <-> i e. { I , J } ) )
168 167 notbid 
 |-  ( ph -> ( -. i e. ran <" I J "> <-> -. i e. { I , J } ) )
169 168 ad2antrr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> ( -. i e. ran <" I J "> <-> -. i e. { I , J } ) )
170 165 169 mpbird 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> -. i e. ran <" I J "> )
171 1 152 154 156 158 170 cycpmfv3 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> ( ( M ` <" I J "> ) ` i ) = i )
172 171 fveq2d 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` W ) ` i ) )
173 3 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( 0 ..^ E ) ) -> D e. V )
174 4 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( 0 ..^ E ) ) -> W e. dom M )
175 5 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( 0 ..^ E ) ) -> I e. ( D \ ran W ) )
176 6 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( 0 ..^ E ) ) -> J e. ran W )
177 simpllr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( 0 ..^ E ) ) -> i e. ran W )
178 simplr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( 0 ..^ E ) ) -> i =/= J )
179 simpr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( 0 ..^ E ) ) -> ( `' U ` i ) e. ( 0 ..^ E ) )
180 1 2 173 174 175 176 7 8 177 178 179 cycpmco2lem7 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( 0 ..^ E ) ) -> ( ( M ` U ) ` i ) = ( ( M ` W ) ` i ) )
181 3 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) -> D e. V )
182 4 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) -> W e. dom M )
183 5 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) -> I e. ( D \ ran W ) )
184 6 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) -> J e. ran W )
185 simpllr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) -> i e. ran W )
186 162 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) -> i =/= I )
187 simpr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) -> ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) )
188 1 2 181 182 183 184 7 8 185 186 187 cycpmco2lem6 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) -> ( ( M ` U ) ` i ) = ( ( M ` W ) ` i ) )
189 3 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) -> D e. V )
190 4 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) -> W e. dom M )
191 5 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) -> I e. ( D \ ran W ) )
192 6 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) -> J e. ran W )
193 simpllr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) -> i e. ran W )
194 simpr 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) -> ( `' U ` i ) = ( ( # ` U ) - 1 ) )
195 1 2 189 190 191 192 7 8 193 194 cycpmco2lem5 
 |-  ( ( ( ( ph /\ i e. ran W ) /\ i =/= J ) /\ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) -> ( ( M ` U ) ` i ) = ( ( M ` W ) ` i ) )
196 f1f1orn 
 |-  ( U : dom U -1-1-> D -> U : dom U -1-1-onto-> ran U )
197 47 196 syl 
 |-  ( ph -> U : dom U -1-1-onto-> ran U )
198 ssun1 
 |-  ran W C_ ( ran W u. { I } )
199 1 2 3 4 5 6 7 8 cycpmco2rn 
 |-  ( ph -> ran U = ( ran W u. { I } ) )
200 198 199 sseqtrrid 
 |-  ( ph -> ran W C_ ran U )
201 200 sselda 
 |-  ( ( ph /\ i e. ran W ) -> i e. ran U )
202 f1ocnvdm 
 |-  ( ( U : dom U -1-1-onto-> ran U /\ i e. ran U ) -> ( `' U ` i ) e. dom U )
203 197 201 202 syl2an2r 
 |-  ( ( ph /\ i e. ran W ) -> ( `' U ` i ) e. dom U )
204 wrddm 
 |-  ( U e. Word D -> dom U = ( 0 ..^ ( # ` U ) ) )
205 46 204 syl 
 |-  ( ph -> dom U = ( 0 ..^ ( # ` U ) ) )
206 205 adantr 
 |-  ( ( ph /\ i e. ran W ) -> dom U = ( 0 ..^ ( # ` U ) ) )
207 203 206 eleqtrd 
 |-  ( ( ph /\ i e. ran W ) -> ( `' U ` i ) e. ( 0 ..^ ( # ` U ) ) )
208 65 nn0zd 
 |-  ( ph -> ( # ` W ) e. ZZ )
209 208 peano2zd 
 |-  ( ph -> ( ( # ` W ) + 1 ) e. ZZ )
210 110 209 eqeltrd 
 |-  ( ph -> ( # ` U ) e. ZZ )
211 fzoval 
 |-  ( ( # ` U ) e. ZZ -> ( 0 ..^ ( # ` U ) ) = ( 0 ... ( ( # ` U ) - 1 ) ) )
212 210 211 syl 
 |-  ( ph -> ( 0 ..^ ( # ` U ) ) = ( 0 ... ( ( # ` U ) - 1 ) ) )
213 212 adantr 
 |-  ( ( ph /\ i e. ran W ) -> ( 0 ..^ ( # ` U ) ) = ( 0 ... ( ( # ` U ) - 1 ) ) )
214 207 213 eleqtrd 
 |-  ( ( ph /\ i e. ran W ) -> ( `' U ` i ) e. ( 0 ... ( ( # ` U ) - 1 ) ) )
215 elfzr 
 |-  ( ( `' U ` i ) e. ( 0 ... ( ( # ` U ) - 1 ) ) -> ( ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) )
216 214 215 syl 
 |-  ( ( ph /\ i e. ran W ) -> ( ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) )
217 simpr 
 |-  ( ( ( ph /\ i e. ran W ) /\ ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) ) -> ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) )
218 99 ad2antrr 
 |-  ( ( ( ph /\ i e. ran W ) /\ ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) ) -> E e. ZZ )
219 fzospliti 
 |-  ( ( ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) /\ E e. ZZ ) -> ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) )
220 217 218 219 syl2anc 
 |-  ( ( ( ph /\ i e. ran W ) /\ ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) ) -> ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) )
221 220 ex 
 |-  ( ( ph /\ i e. ran W ) -> ( ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) -> ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) ) )
222 221 orim1d 
 |-  ( ( ph /\ i e. ran W ) -> ( ( ( `' U ` i ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) -> ( ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) ) )
223 216 222 mpd 
 |-  ( ( ph /\ i e. ran W ) -> ( ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) )
224 df-3or 
 |-  ( ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) <-> ( ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) )
225 223 224 sylibr 
 |-  ( ( ph /\ i e. ran W ) -> ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) )
226 225 adantr 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> ( ( `' U ` i ) e. ( 0 ..^ E ) \/ ( `' U ` i ) e. ( E ..^ ( ( # ` U ) - 1 ) ) \/ ( `' U ` i ) = ( ( # ` U ) - 1 ) ) )
227 180 188 195 226 mpjao3dan 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> ( ( M ` U ) ` i ) = ( ( M ` W ) ` i ) )
228 172 227 eqtr4d 
 |-  ( ( ( ph /\ i e. ran W ) /\ i =/= J ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
229 151 228 pm2.61dane 
 |-  ( ( ph /\ i e. ran W ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
230 229 adantlr 
 |-  ( ( ( ph /\ i e. D ) /\ i e. ran W ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
231 1 2 3 4 5 6 7 8 cycpmco2lem4 
 |-  ( ph -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` I ) ) = ( ( M ` U ) ` I ) )
232 231 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i = I ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` I ) ) = ( ( M ` U ) ` I ) )
233 simpr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i = I ) -> i = I )
234 233 fveq2d 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i = I ) -> ( ( M ` <" I J "> ) ` i ) = ( ( M ` <" I J "> ) ` I ) )
235 234 fveq2d 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i = I ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` W ) ` ( ( M ` <" I J "> ) ` I ) ) )
236 233 fveq2d 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i = I ) -> ( ( M ` U ) ` i ) = ( ( M ` U ) ` I ) )
237 232 235 236 3eqtr4d 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i = I ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
238 3 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> D e. V )
239 20 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> W e. Word D )
240 27 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> W : dom W -1-1-> D )
241 simplr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> i e. ( D \ ran W ) )
242 241 eldifad 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> i e. D )
243 241 eldifbd 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> -. i e. ran W )
244 1 238 239 240 242 243 cycpmfv3 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> ( ( M ` W ) ` i ) = i )
245 153 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> <" I J "> e. Word D )
246 155 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> <" I J "> : dom <" I J "> -1-1-> D )
247 simpr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> i =/= I )
248 eldifn 
 |-  ( i e. ( D \ ran W ) -> -. i e. ran W )
249 nelne2 
 |-  ( ( J e. ran W /\ -. i e. ran W ) -> J =/= i )
250 6 248 249 syl2an 
 |-  ( ( ph /\ i e. ( D \ ran W ) ) -> J =/= i )
251 250 necomd 
 |-  ( ( ph /\ i e. ( D \ ran W ) ) -> i =/= J )
252 251 adantr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> i =/= J )
253 247 252 nelprd 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> -. i e. { I , J } )
254 168 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> ( -. i e. ran <" I J "> <-> -. i e. { I , J } ) )
255 253 254 mpbird 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> -. i e. ran <" I J "> )
256 1 238 245 246 242 255 cycpmfv3 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> ( ( M ` <" I J "> ) ` i ) = i )
257 256 fveq2d 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` W ) ` i ) )
258 46 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> U e. Word D )
259 47 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> U : dom U -1-1-> D )
260 199 ad2antrr 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> ran U = ( ran W u. { I } ) )
261 nelsn 
 |-  ( i =/= I -> -. i e. { I } )
262 261 adantl 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> -. i e. { I } )
263 nelun 
 |-  ( ran U = ( ran W u. { I } ) -> ( -. i e. ran U <-> ( -. i e. ran W /\ -. i e. { I } ) ) )
264 263 biimpar 
 |-  ( ( ran U = ( ran W u. { I } ) /\ ( -. i e. ran W /\ -. i e. { I } ) ) -> -. i e. ran U )
265 260 243 262 264 syl12anc 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> -. i e. ran U )
266 1 238 258 259 242 265 cycpmfv3 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> ( ( M ` U ) ` i ) = i )
267 244 257 266 3eqtr4d 
 |-  ( ( ( ph /\ i e. ( D \ ran W ) ) /\ i =/= I ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
268 237 267 pm2.61dane 
 |-  ( ( ph /\ i e. ( D \ ran W ) ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
269 268 adantlr 
 |-  ( ( ( ph /\ i e. D ) /\ i e. ( D \ ran W ) ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
270 undif 
 |-  ( ran W C_ D <-> ( ran W u. ( D \ ran W ) ) = D )
271 30 270 sylib 
 |-  ( ph -> ( ran W u. ( D \ ran W ) ) = D )
272 271 eleq2d 
 |-  ( ph -> ( i e. ( ran W u. ( D \ ran W ) ) <-> i e. D ) )
273 elun 
 |-  ( i e. ( ran W u. ( D \ ran W ) ) <-> ( i e. ran W \/ i e. ( D \ ran W ) ) )
274 272 273 bitr3di 
 |-  ( ph -> ( i e. D <-> ( i e. ran W \/ i e. ( D \ ran W ) ) ) )
275 274 biimpa 
 |-  ( ( ph /\ i e. D ) -> ( i e. ran W \/ i e. ( D \ ran W ) ) )
276 230 269 275 mpjaodan 
 |-  ( ( ph /\ i e. D ) -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` i ) ) = ( ( M ` U ) ` i ) )
277 53 276 eqtrd 
 |-  ( ( ph /\ i e. D ) -> ( ( ( M ` W ) o. ( M ` <" I J "> ) ) ` i ) = ( ( M ` U ) ` i ) )
278 42 51 277 eqfnfvd 
 |-  ( ph -> ( ( M ` W ) o. ( M ` <" I J "> ) ) = ( M ` U ) )