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
|
sseldi |
|- ( 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
|
sseldi |
|- ( 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 ) ) |