Metamath Proof Explorer

Theorem cycpmco2lem6

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 )
cycpmco2lem6.2 
|- ( ph -> K =/= I )
cycpmco2lem6.1 
|- ( ph -> ( `' U ` K ) e. ( E ..^ ( ( # ` U ) - 1 ) ) )
Assertion cycpmco2lem6 
|- ( 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 cycpmco2lem6.2 
 |-  ( ph -> K =/= I )
11 cycpmco2lem6.1 
 |-  ( ph -> ( `' U ` K ) e. ( E ..^ ( ( # ` U ) - 1 ) ) )
12 ssrab2 
 |-  { w e. Word D | w : dom w -1-1-> D } C_ Word D
13 eqid 
 |-  ( Base ` S ) = ( Base ` S )
14 1 2 13 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
15 3 14 syl 
 |-  ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
16 15 fdmd 
 |-  ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
17 4 16 eleqtrd 
 |-  ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
18 12 17 sselid 
 |-  ( ph -> W e. Word D )
19 5 eldifad 
 |-  ( ph -> I e. D )
20 19 s1cld 
 |-  ( ph -> <" I "> e. Word D )
21 splcl 
 |-  ( ( W e. Word D /\ <" I "> e. Word D ) -> ( W splice <. E , E , <" I "> >. ) e. Word D )
22 18 20 21 syl2anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) e. Word D )
23 8 22 eqeltrid 
 |-  ( ph -> U e. Word D )
24 1 2 3 4 5 6 7 8 cycpmco2f1 
 |-  ( ph -> U : dom U -1-1-> D )
25 fz0ssnn0 
 |-  ( 0 ... ( # ` W ) ) C_ NN0
26 id 
 |-  ( w = W -> w = W )
27 dmeq 
 |-  ( w = W -> dom w = dom W )
28 eqidd 
 |-  ( w = W -> D = D )
29 26 27 28 f1eq123d 
 |-  ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
30 29 elrab 
 |-  ( W e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
31 17 30 sylib 
 |-  ( ph -> ( W e. Word D /\ W : dom W -1-1-> D ) )
32 31 simprd 
 |-  ( ph -> W : dom W -1-1-> D )
33 f1cnv 
 |-  ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
34 f1of 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
35 32 33 34 3syl 
 |-  ( ph -> `' W : ran W --> dom W )
36 35 6 ffvelrnd 
 |-  ( ph -> ( `' W ` J ) e. dom W )
37 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
38 18 37 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
39 36 38 eleqtrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
40 fzofzp1 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
41 39 40 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
42 7 41 eqeltrid 
 |-  ( ph -> E e. ( 0 ... ( # ` W ) ) )
43 25 42 sselid 
 |-  ( ph -> E e. NN0 )
44 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
45 43 44 eleqtrdi 
 |-  ( ph -> E e. ( ZZ>= ` 0 ) )
46 fzoss1 
 |-  ( E e. ( ZZ>= ` 0 ) -> ( E ..^ ( ( # ` U ) - 1 ) ) C_ ( 0 ..^ ( ( # ` U ) - 1 ) ) )
47 45 46 syl 
 |-  ( ph -> ( E ..^ ( ( # ` U ) - 1 ) ) C_ ( 0 ..^ ( ( # ` U ) - 1 ) ) )
48 47 11 sseldd 
 |-  ( ph -> ( `' U ` K ) e. ( 0 ..^ ( ( # ` U ) - 1 ) ) )
49 1 3 23 24 48 cycpmfv1 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( `' U ` K ) ) ) = ( U ` ( ( `' U ` K ) + 1 ) ) )
50 f1f1orn 
 |-  ( U : dom U -1-1-> D -> U : dom U -1-1-onto-> ran U )
51 24 50 syl 
 |-  ( ph -> U : dom U -1-1-onto-> ran U )
52 ssun1 
 |-  ran W C_ ( ran W u. { I } )
53 1 2 3 4 5 6 7 8 cycpmco2rn 
 |-  ( ph -> ran U = ( ran W u. { I } ) )
54 52 53 sseqtrrid 
 |-  ( ph -> ran W C_ ran U )
55 54 sselda 
 |-  ( ( ph /\ K e. ran W ) -> K e. ran U )
56 f1ocnvfv2 
 |-  ( ( U : dom U -1-1-onto-> ran U /\ K e. ran U ) -> ( U ` ( `' U ` K ) ) = K )
57 51 55 56 syl2an2r 
 |-  ( ( ph /\ K e. ran W ) -> ( U ` ( `' U ` K ) ) = K )
58 9 57 mpdan 
 |-  ( ph -> ( U ` ( `' U ` K ) ) = K )
59 58 fveq2d 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( `' U ` K ) ) ) = ( ( M ` U ) ` K ) )
60 8 a1i 
 |-  ( ph -> U = ( W splice <. E , E , <" I "> >. ) )
61 fzossz 
 |-  ( E ..^ ( ( # ` U ) - 1 ) ) C_ ZZ
62 61 11 sselid 
 |-  ( ph -> ( `' U ` K ) e. ZZ )
63 62 zcnd 
 |-  ( ph -> ( `' U ` K ) e. CC )
64 43 nn0cnd 
 |-  ( ph -> E e. CC )
65 1cnd 
 |-  ( ph -> 1 e. CC )
66 63 64 65 nppcan3d 
 |-  ( ph -> ( ( ( `' U ` K ) - E ) + ( 1 + E ) ) = ( ( `' U ` K ) + 1 ) )
67 66 eqcomd 
 |-  ( ph -> ( ( `' U ` K ) + 1 ) = ( ( ( `' U ` K ) - E ) + ( 1 + E ) ) )
68 60 67 fveq12d 
 |-  ( ph -> ( U ` ( ( `' U ` K ) + 1 ) ) = ( ( W splice <. E , E , <" I "> >. ) ` ( ( ( `' U ` K ) - E ) + ( 1 + E ) ) ) )
69 49 59 68 3eqtr3d 
 |-  ( ph -> ( ( M ` U ) ` K ) = ( ( W splice <. E , E , <" I "> >. ) ` ( ( ( `' U ` K ) - E ) + ( 1 + E ) ) ) )
70 63 64 npcand 
 |-  ( ph -> ( ( ( `' U ` K ) - E ) + E ) = ( `' U ` K ) )
71 70 fveq2d 
 |-  ( ph -> ( W ` ( ( ( `' U ` K ) - E ) + E ) ) = ( W ` ( `' U ` K ) ) )
72 nn0fz0 
 |-  ( E e. NN0 <-> E e. ( 0 ... E ) )
73 43 72 sylib 
 |-  ( ph -> E e. ( 0 ... E ) )
74 lencl 
 |-  ( W e. Word D -> ( # ` W ) e. NN0 )
75 18 74 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
76 75 nn0cnd 
 |-  ( ph -> ( # ` W ) e. CC )
77 ovexd 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. _V )
78 7 77 eqeltrid 
 |-  ( ph -> E e. _V )
79 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 ) >. ) ) )
80 4 78 78 20 79 syl13anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
81 8 80 syl5eq 
 |-  ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
82 81 fveq2d 
 |-  ( ph -> ( # ` U ) = ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) )
83 pfxcl 
 |-  ( W e. Word D -> ( W prefix E ) e. Word D )
84 18 83 syl 
 |-  ( ph -> ( W prefix E ) e. Word D )
85 ccatcl 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
86 84 20 85 syl2anc 
 |-  ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
87 swrdcl 
 |-  ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
88 18 87 syl 
 |-  ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
89 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 ) >. ) ) ) )
90 86 88 89 syl2anc 
 |-  ( ph -> ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) )
91 ccatws1len 
 |-  ( ( W prefix E ) e. Word D -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
92 18 83 91 3syl 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
93 pfxlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix E ) ) = E )
94 18 42 93 syl2anc 
 |-  ( ph -> ( # ` ( W prefix E ) ) = E )
95 94 oveq1d 
 |-  ( ph -> ( ( # ` ( W prefix E ) ) + 1 ) = ( E + 1 ) )
96 92 95 eqtrd 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( E + 1 ) )
97 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
98 75 97 sylib 
 |-  ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
99 swrdlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
100 18 42 98 99 syl3anc 
 |-  ( ph -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
101 96 100 oveq12d 
 |-  ( ph -> ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
102 82 90 101 3eqtrd 
 |-  ( ph -> ( # ` U ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
103 43 nn0zd 
 |-  ( ph -> E e. ZZ )
104 103 peano2zd 
 |-  ( ph -> ( E + 1 ) e. ZZ )
105 104 zcnd 
 |-  ( ph -> ( E + 1 ) e. CC )
106 105 76 64 addsubassd 
 |-  ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
107 64 65 76 addassd 
 |-  ( ph -> ( ( E + 1 ) + ( # ` W ) ) = ( E + ( 1 + ( # ` W ) ) ) )
108 107 oveq1d 
 |-  ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
109 102 106 108 3eqtr2d 
 |-  ( ph -> ( # ` U ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
110 65 76 addcld 
 |-  ( ph -> ( 1 + ( # ` W ) ) e. CC )
111 64 110 pncan2d 
 |-  ( ph -> ( ( E + ( 1 + ( # ` W ) ) ) - E ) = ( 1 + ( # ` W ) ) )
112 65 76 addcomd 
 |-  ( ph -> ( 1 + ( # ` W ) ) = ( ( # ` W ) + 1 ) )
113 109 111 112 3eqtrd 
 |-  ( ph -> ( # ` U ) = ( ( # ` W ) + 1 ) )
114 76 65 113 mvrraddd 
 |-  ( ph -> ( ( # ` U ) - 1 ) = ( # ` W ) )
115 114 oveq2d 
 |-  ( ph -> ( E ..^ ( ( # ` U ) - 1 ) ) = ( E ..^ ( # ` W ) ) )
116 11 115 eleqtrd 
 |-  ( ph -> ( `' U ` K ) e. ( E ..^ ( # ` W ) ) )
117 fzosubel 
 |-  ( ( ( `' U ` K ) e. ( E ..^ ( # ` W ) ) /\ E e. ZZ ) -> ( ( `' U ` K ) - E ) e. ( ( E - E ) ..^ ( ( # ` W ) - E ) ) )
118 116 103 117 syl2anc 
 |-  ( ph -> ( ( `' U ` K ) - E ) e. ( ( E - E ) ..^ ( ( # ` W ) - E ) ) )
119 64 subidd 
 |-  ( ph -> ( E - E ) = 0 )
120 119 oveq1d 
 |-  ( ph -> ( ( E - E ) ..^ ( ( # ` W ) - E ) ) = ( 0 ..^ ( ( # ` W ) - E ) ) )
121 118 120 eleqtrd 
 |-  ( ph -> ( ( `' U ` K ) - E ) e. ( 0 ..^ ( ( # ` W ) - E ) ) )
122 65 64 addcomd 
 |-  ( ph -> ( 1 + E ) = ( E + 1 ) )
123 s1len 
 |-  ( # ` <" I "> ) = 1
124 123 oveq2i 
 |-  ( E + ( # ` <" I "> ) ) = ( E + 1 )
125 122 124 eqtr4di 
 |-  ( ph -> ( 1 + E ) = ( E + ( # ` <" I "> ) ) )
126 18 73 42 20 121 125 splfv3 
 |-  ( ph -> ( ( W splice <. E , E , <" I "> >. ) ` ( ( ( `' U ` K ) - E ) + ( 1 + E ) ) ) = ( W ` ( ( ( `' U ` K ) - E ) + E ) ) )
127 114 oveq1d 
 |-  ( ph -> ( ( ( # ` U ) - 1 ) - 1 ) = ( ( # ` W ) - 1 ) )
128 127 oveq2d 
 |-  ( ph -> ( E ..^ ( ( ( # ` U ) - 1 ) - 1 ) ) = ( E ..^ ( ( # ` W ) - 1 ) ) )
129 fzoss1 
 |-  ( E e. ( ZZ>= ` 0 ) -> ( E ..^ ( ( # ` W ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
130 45 129 syl 
 |-  ( ph -> ( E ..^ ( ( # ` W ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
131 128 130 eqsstrd 
 |-  ( ph -> ( E ..^ ( ( ( # ` U ) - 1 ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
132 f1ocnvdm 
 |-  ( ( U : dom U -1-1-onto-> ran U /\ K e. ran U ) -> ( `' U ` K ) e. dom U )
133 51 55 132 syl2an2r 
 |-  ( ( ph /\ K e. ran W ) -> ( `' U ` K ) e. dom U )
134 9 133 mpdan 
 |-  ( ph -> ( `' U ` K ) e. dom U )
135 75 nn0zd 
 |-  ( ph -> ( # ` W ) e. ZZ )
136 135 peano2zd 
 |-  ( ph -> ( ( # ` W ) + 1 ) e. ZZ )
137 elfzonn0 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( `' W ` J ) e. NN0 )
138 nn0p1nn 
 |-  ( ( `' W ` J ) e. NN0 -> ( ( `' W ` J ) + 1 ) e. NN )
139 39 137 138 3syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. NN )
140 7 139 eqeltrid 
 |-  ( ph -> E e. NN )
141 140 nnred 
 |-  ( ph -> E e. RR )
142 135 zred 
 |-  ( ph -> ( # ` W ) e. RR )
143 1red 
 |-  ( ph -> 1 e. RR )
144 elfzle2 
 |-  ( E e. ( 0 ... ( # ` W ) ) -> E <_ ( # ` W ) )
145 42 144 syl 
 |-  ( ph -> E <_ ( # ` W ) )
146 141 142 143 145 leadd1dd 
 |-  ( ph -> ( E + 1 ) <_ ( ( # ` W ) + 1 ) )
147 eluz2 
 |-  ( ( ( # ` W ) + 1 ) e. ( ZZ>= ` ( E + 1 ) ) <-> ( ( E + 1 ) e. ZZ /\ ( ( # ` W ) + 1 ) e. ZZ /\ ( E + 1 ) <_ ( ( # ` W ) + 1 ) ) )
148 104 136 146 147 syl3anbrc 
 |-  ( ph -> ( ( # ` W ) + 1 ) e. ( ZZ>= ` ( E + 1 ) ) )
149 fzoss2 
 |-  ( ( ( # ` W ) + 1 ) e. ( ZZ>= ` ( E + 1 ) ) -> ( 0 ..^ ( E + 1 ) ) C_ ( 0 ..^ ( ( # ` W ) + 1 ) ) )
150 148 149 syl 
 |-  ( ph -> ( 0 ..^ ( E + 1 ) ) C_ ( 0 ..^ ( ( # ` W ) + 1 ) ) )
151 fzonn0p1 
 |-  ( E e. NN0 -> E e. ( 0 ..^ ( E + 1 ) ) )
152 43 151 syl 
 |-  ( ph -> E e. ( 0 ..^ ( E + 1 ) ) )
153 150 152 sseldd 
 |-  ( ph -> E e. ( 0 ..^ ( ( # ` W ) + 1 ) ) )
154 113 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` U ) ) = ( 0 ..^ ( ( # ` W ) + 1 ) ) )
155 153 154 eleqtrrd 
 |-  ( ph -> E e. ( 0 ..^ ( # ` U ) ) )
156 wrddm 
 |-  ( U e. Word D -> dom U = ( 0 ..^ ( # ` U ) ) )
157 23 156 syl 
 |-  ( ph -> dom U = ( 0 ..^ ( # ` U ) ) )
158 155 157 eleqtrrd 
 |-  ( ph -> E e. dom U )
159 1 2 3 4 5 6 7 8 cycpmco2lem2 
 |-  ( ph -> ( U ` E ) = I )
160 10 58 159 3netr4d 
 |-  ( ph -> ( U ` ( `' U ` K ) ) =/= ( U ` E ) )
161 f1fveq 
 |-  ( ( U : dom U -1-1-> D /\ ( ( `' U ` K ) e. dom U /\ E e. dom U ) ) -> ( ( U ` ( `' U ` K ) ) = ( U ` E ) <-> ( `' U ` K ) = E ) )
162 161 necon3bid 
 |-  ( ( U : dom U -1-1-> D /\ ( ( `' U ` K ) e. dom U /\ E e. dom U ) ) -> ( ( U ` ( `' U ` K ) ) =/= ( U ` E ) <-> ( `' U ` K ) =/= E ) )
163 162 biimp3a 
 |-  ( ( U : dom U -1-1-> D /\ ( ( `' U ` K ) e. dom U /\ E e. dom U ) /\ ( U ` ( `' U ` K ) ) =/= ( U ` E ) ) -> ( `' U ` K ) =/= E )
164 24 134 158 160 163 syl121anc 
 |-  ( ph -> ( `' U ` K ) =/= E )
165 fzom1ne1 
 |-  ( ( ( `' U ` K ) e. ( E ..^ ( ( # ` U ) - 1 ) ) /\ ( `' U ` K ) =/= E ) -> ( ( `' U ` K ) - 1 ) e. ( E ..^ ( ( ( # ` U ) - 1 ) - 1 ) ) )
166 11 164 165 syl2anc 
 |-  ( ph -> ( ( `' U ` K ) - 1 ) e. ( E ..^ ( ( ( # ` U ) - 1 ) - 1 ) ) )
167 131 166 sseldd 
 |-  ( ph -> ( ( `' U ` K ) - 1 ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
168 1 3 18 32 167 cycpmfv1 
 |-  ( ph -> ( ( M ` W ) ` ( W ` ( ( `' U ` K ) - 1 ) ) ) = ( W ` ( ( ( `' U ` K ) - 1 ) + 1 ) ) )
169 63 65 64 subsub4d 
 |-  ( ph -> ( ( ( `' U ` K ) - 1 ) - E ) = ( ( `' U ` K ) - ( 1 + E ) ) )
170 169 oveq1d 
 |-  ( ph -> ( ( ( ( `' U ` K ) - 1 ) - E ) + ( 1 + E ) ) = ( ( ( `' U ` K ) - ( 1 + E ) ) + ( 1 + E ) ) )
171 65 64 addcld 
 |-  ( ph -> ( 1 + E ) e. CC )
172 63 171 npcand 
 |-  ( ph -> ( ( ( `' U ` K ) - ( 1 + E ) ) + ( 1 + E ) ) = ( `' U ` K ) )
173 170 172 eqtr2d 
 |-  ( ph -> ( `' U ` K ) = ( ( ( ( `' U ` K ) - 1 ) - E ) + ( 1 + E ) ) )
174 60 173 fveq12d 
 |-  ( ph -> ( U ` ( `' U ` K ) ) = ( ( W splice <. E , E , <" I "> >. ) ` ( ( ( ( `' U ` K ) - 1 ) - E ) + ( 1 + E ) ) ) )
175 64 76 pncan3d 
 |-  ( ph -> ( E + ( ( # ` W ) - E ) ) = ( # ` W ) )
176 114 135 eqeltrd 
 |-  ( ph -> ( ( # ` U ) - 1 ) e. ZZ )
177 1zzd 
 |-  ( ph -> 1 e. ZZ )
178 176 177 zsubcld 
 |-  ( ph -> ( ( ( # ` U ) - 1 ) - 1 ) e. ZZ )
179 178 zred 
 |-  ( ph -> ( ( ( # ` U ) - 1 ) - 1 ) e. RR )
180 114 142 eqeltrd 
 |-  ( ph -> ( ( # ` U ) - 1 ) e. RR )
181 180 ltm1d 
 |-  ( ph -> ( ( ( # ` U ) - 1 ) - 1 ) < ( ( # ` U ) - 1 ) )
182 181 114 breqtrd 
 |-  ( ph -> ( ( ( # ` U ) - 1 ) - 1 ) < ( # ` W ) )
183 179 142 182 ltled 
 |-  ( ph -> ( ( ( # ` U ) - 1 ) - 1 ) <_ ( # ` W ) )
184 eluz1 
 |-  ( ( ( ( # ` U ) - 1 ) - 1 ) e. ZZ -> ( ( # ` W ) e. ( ZZ>= ` ( ( ( # ` U ) - 1 ) - 1 ) ) <-> ( ( # ` W ) e. ZZ /\ ( ( ( # ` U ) - 1 ) - 1 ) <_ ( # ` W ) ) ) )
185 184 biimpar 
 |-  ( ( ( ( ( # ` U ) - 1 ) - 1 ) e. ZZ /\ ( ( # ` W ) e. ZZ /\ ( ( ( # ` U ) - 1 ) - 1 ) <_ ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` ( ( ( # ` U ) - 1 ) - 1 ) ) )
186 178 135 183 185 syl12anc 
 |-  ( ph -> ( # ` W ) e. ( ZZ>= ` ( ( ( # ` U ) - 1 ) - 1 ) ) )
187 175 186 eqeltrd 
 |-  ( ph -> ( E + ( ( # ` W ) - E ) ) e. ( ZZ>= ` ( ( ( # ` U ) - 1 ) - 1 ) ) )
188 fzoss2 
 |-  ( ( E + ( ( # ` W ) - E ) ) e. ( ZZ>= ` ( ( ( # ` U ) - 1 ) - 1 ) ) -> ( E ..^ ( ( ( # ` U ) - 1 ) - 1 ) ) C_ ( E ..^ ( E + ( ( # ` W ) - E ) ) ) )
189 187 188 syl 
 |-  ( ph -> ( E ..^ ( ( ( # ` U ) - 1 ) - 1 ) ) C_ ( E ..^ ( E + ( ( # ` W ) - E ) ) ) )
190 189 166 sseldd 
 |-  ( ph -> ( ( `' U ` K ) - 1 ) e. ( E ..^ ( E + ( ( # ` W ) - E ) ) ) )
191 135 103 zsubcld 
 |-  ( ph -> ( ( # ` W ) - E ) e. ZZ )
192 fzosubel3 
 |-  ( ( ( ( `' U ` K ) - 1 ) e. ( E ..^ ( E + ( ( # ` W ) - E ) ) ) /\ ( ( # ` W ) - E ) e. ZZ ) -> ( ( ( `' U ` K ) - 1 ) - E ) e. ( 0 ..^ ( ( # ` W ) - E ) ) )
193 190 191 192 syl2anc 
 |-  ( ph -> ( ( ( `' U ` K ) - 1 ) - E ) e. ( 0 ..^ ( ( # ` W ) - E ) ) )
194 18 73 42 20 193 125 splfv3 
 |-  ( ph -> ( ( W splice <. E , E , <" I "> >. ) ` ( ( ( ( `' U ` K ) - 1 ) - E ) + ( 1 + E ) ) ) = ( W ` ( ( ( ( `' U ` K ) - 1 ) - E ) + E ) ) )
195 63 65 subcld 
 |-  ( ph -> ( ( `' U ` K ) - 1 ) e. CC )
196 195 64 npcand 
 |-  ( ph -> ( ( ( ( `' U ` K ) - 1 ) - E ) + E ) = ( ( `' U ` K ) - 1 ) )
197 196 fveq2d 
 |-  ( ph -> ( W ` ( ( ( ( `' U ` K ) - 1 ) - E ) + E ) ) = ( W ` ( ( `' U ` K ) - 1 ) ) )
198 174 194 197 3eqtrd 
 |-  ( ph -> ( U ` ( `' U ` K ) ) = ( W ` ( ( `' U ` K ) - 1 ) ) )
199 198 58 eqtr3d 
 |-  ( ph -> ( W ` ( ( `' U ` K ) - 1 ) ) = K )
200 199 fveq2d 
 |-  ( ph -> ( ( M ` W ) ` ( W ` ( ( `' U ` K ) - 1 ) ) ) = ( ( M ` W ) ` K ) )
201 63 65 npcand 
 |-  ( ph -> ( ( ( `' U ` K ) - 1 ) + 1 ) = ( `' U ` K ) )
202 201 fveq2d 
 |-  ( ph -> ( W ` ( ( ( `' U ` K ) - 1 ) + 1 ) ) = ( W ` ( `' U ` K ) ) )
203 168 200 202 3eqtr3d 
 |-  ( ph -> ( ( M ` W ) ` K ) = ( W ` ( `' U ` K ) ) )
204 71 126 203 3eqtr4rd 
 |-  ( ph -> ( ( M ` W ) ` K ) = ( ( W splice <. E , E , <" I "> >. ) ` ( ( ( `' U ` K ) - E ) + ( 1 + E ) ) ) )
205 69 204 eqtr4d 
 |-  ( ph -> ( ( M ` U ) ` K ) = ( ( M ` W ) ` K ) )