Metamath Proof Explorer

Theorem cycpmco2lem7

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 "> >. )
cycpmco2lem7.1 
|- ( ph -> K e. ran W )
cycpmco2lem7.2 
|- ( ph -> K =/= J )
cycpmco2lem7.3 
|- ( ph -> ( `' U ` K ) e. ( 0 ..^ E ) )
Assertion cycpmco2lem7 
|- ( 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 cycpmco2lem7.1 
 |-  ( ph -> K e. ran W )
10 cycpmco2lem7.2 
 |-  ( ph -> K =/= J )
11 cycpmco2lem7.3 
 |-  ( ph -> ( `' U ` K ) e. ( 0 ..^ E ) )
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 id 
 |-  ( w = W -> w = W )
26 dmeq 
 |-  ( w = W -> dom w = dom W )
27 eqidd 
 |-  ( w = W -> D = D )
28 25 26 27 f1eq123d 
 |-  ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
29 28 elrab 
 |-  ( W e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
30 17 29 sylib 
 |-  ( ph -> ( W e. Word D /\ W : dom W -1-1-> D ) )
31 30 simprd 
 |-  ( ph -> W : dom W -1-1-> D )
32 f1cnv 
 |-  ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
33 f1of 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
34 31 32 33 3syl 
 |-  ( ph -> `' W : ran W --> dom W )
35 34 6 ffvelcdmd 
 |-  ( ph -> ( `' W ` J ) e. dom W )
36 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
37 18 36 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
38 35 37 eleqtrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
39 fzofzp1 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
40 38 39 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
41 7 40 eqeltrid 
 |-  ( ph -> E e. ( 0 ... ( # ` W ) ) )
42 elfzuz3 
 |-  ( E e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` E ) )
43 fzoss2 
 |-  ( ( # ` W ) e. ( ZZ>= ` E ) -> ( 0 ..^ E ) C_ ( 0 ..^ ( # ` W ) ) )
44 41 42 43 3syl 
 |-  ( ph -> ( 0 ..^ E ) C_ ( 0 ..^ ( # ` W ) ) )
45 1 2 3 4 5 6 7 8 cycpmco2lem3 
 |-  ( ph -> ( ( # ` U ) - 1 ) = ( # ` W ) )
46 45 oveq2d 
 |-  ( ph -> ( 0 ..^ ( ( # ` U ) - 1 ) ) = ( 0 ..^ ( # ` W ) ) )
47 44 46 sseqtrrd 
 |-  ( ph -> ( 0 ..^ E ) 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 57 fveq2d 
 |-  ( ( ph /\ K e. ran W ) -> ( ( M ` U ) ` ( U ` ( `' U ` K ) ) ) = ( ( M ` U ) ` K ) )
59 9 58 mpdan 
 |-  ( ph -> ( ( M ` U ) ` ( U ` ( `' U ` K ) ) ) = ( ( M ` U ) ` K ) )
60 f1f1orn 
 |-  ( W : dom W -1-1-> D -> W : dom W -1-1-onto-> ran W )
61 31 60 syl 
 |-  ( ph -> W : dom W -1-1-onto-> ran W )
62 44 37 sseqtrrd 
 |-  ( ph -> ( 0 ..^ E ) C_ dom W )
63 62 11 sseldd 
 |-  ( ph -> ( `' U ` K ) e. dom W )
64 f1ocnvfv1 
 |-  ( ( W : dom W -1-1-onto-> ran W /\ ( `' U ` K ) e. dom W ) -> ( `' W ` ( W ` ( `' U ` K ) ) ) = ( `' U ` K ) )
65 61 63 64 syl2anc 
 |-  ( ph -> ( `' W ` ( W ` ( `' U ` K ) ) ) = ( `' U ` K ) )
66 8 fveq1i 
 |-  ( U ` ( `' U ` K ) ) = ( ( W splice <. E , E , <" I "> >. ) ` ( `' U ` K ) )
67 fz0ssnn0 
 |-  ( 0 ... ( # ` W ) ) C_ NN0
68 67 41 sselid 
 |-  ( ph -> E e. NN0 )
69 nn0fz0 
 |-  ( E e. NN0 <-> E e. ( 0 ... E ) )
70 68 69 sylib 
 |-  ( ph -> E e. ( 0 ... E ) )
71 18 70 41 20 11 splfv1 
 |-  ( ph -> ( ( W splice <. E , E , <" I "> >. ) ` ( `' U ` K ) ) = ( W ` ( `' U ` K ) ) )
72 66 71 eqtrid 
 |-  ( ph -> ( U ` ( `' U ` K ) ) = ( W ` ( `' U ` K ) ) )
73 9 57 mpdan 
 |-  ( ph -> ( U ` ( `' U ` K ) ) = K )
74 72 73 eqtr3d 
 |-  ( ph -> ( W ` ( `' U ` K ) ) = K )
75 74 fveq2d 
 |-  ( ph -> ( `' W ` ( W ` ( `' U ` K ) ) ) = ( `' W ` K ) )
76 65 75 eqtr3d 
 |-  ( ph -> ( `' U ` K ) = ( `' W ` K ) )
77 76 oveq1d 
 |-  ( ph -> ( ( `' U ` K ) + 1 ) = ( ( `' W ` K ) + 1 ) )
78 77 fveq2d 
 |-  ( ph -> ( U ` ( ( `' U ` K ) + 1 ) ) = ( U ` ( ( `' W ` K ) + 1 ) ) )
79 49 59 78 3eqtr3d 
 |-  ( ph -> ( ( M ` U ) ` K ) = ( U ` ( ( `' W ` K ) + 1 ) ) )
80 8 a1i 
 |-  ( ph -> U = ( W splice <. E , E , <" I "> >. ) )
81 80 fveq1d 
 |-  ( ph -> ( U ` ( ( `' W ` K ) + 1 ) ) = ( ( W splice <. E , E , <" I "> >. ) ` ( ( `' W ` K ) + 1 ) ) )
82 41 elfzelzd 
 |-  ( ph -> E e. ZZ )
83 simpr 
 |-  ( ( ph /\ ( `' U ` K ) e. ( 0 ..^ ( E - 1 ) ) ) -> ( `' U ` K ) e. ( 0 ..^ ( E - 1 ) ) )
84 7 a1i 
 |-  ( ph -> E = ( ( `' W ` J ) + 1 ) )
85 84 oveq1d 
 |-  ( ph -> ( E - 1 ) = ( ( ( `' W ` J ) + 1 ) - 1 ) )
86 elfzonn0 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( `' W ` J ) e. NN0 )
87 38 86 syl 
 |-  ( ph -> ( `' W ` J ) e. NN0 )
88 87 nn0cnd 
 |-  ( ph -> ( `' W ` J ) e. CC )
89 1cnd 
 |-  ( ph -> 1 e. CC )
90 88 89 pncand 
 |-  ( ph -> ( ( ( `' W ` J ) + 1 ) - 1 ) = ( `' W ` J ) )
91 85 90 eqtr2d 
 |-  ( ph -> ( `' W ` J ) = ( E - 1 ) )
92 91 adantr 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> ( `' W ` J ) = ( E - 1 ) )
93 simpr 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> ( `' U ` K ) = ( E - 1 ) )
94 76 adantr 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> ( `' U ` K ) = ( `' W ` K ) )
95 92 93 94 3eqtr2rd 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> ( `' W ` K ) = ( `' W ` J ) )
96 95 fveq2d 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> ( W ` ( `' W ` K ) ) = ( W ` ( `' W ` J ) ) )
97 f1ocnvfv2 
 |-  ( ( W : dom W -1-1-onto-> ran W /\ K e. ran W ) -> ( W ` ( `' W ` K ) ) = K )
98 61 9 97 syl2anc 
 |-  ( ph -> ( W ` ( `' W ` K ) ) = K )
99 98 adantr 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> ( W ` ( `' W ` K ) ) = K )
100 f1ocnvfv2 
 |-  ( ( W : dom W -1-1-onto-> ran W /\ J e. ran W ) -> ( W ` ( `' W ` J ) ) = J )
101 61 6 100 syl2anc 
 |-  ( ph -> ( W ` ( `' W ` J ) ) = J )
102 101 adantr 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> ( W ` ( `' W ` J ) ) = J )
103 96 99 102 3eqtr3d 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> K = J )
104 10 adantr 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> K =/= J )
105 103 104 pm2.21ddne 
 |-  ( ( ph /\ ( `' U ` K ) = ( E - 1 ) ) -> ( `' U ` K ) e. ( 0 ..^ ( E - 1 ) ) )
106 0zd 
 |-  ( ph -> 0 e. ZZ )
107 nn0p1nn 
 |-  ( ( `' W ` J ) e. NN0 -> ( ( `' W ` J ) + 1 ) e. NN )
108 87 107 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. NN )
109 7 108 eqeltrid 
 |-  ( ph -> E e. NN )
110 0p1e1 
 |-  ( 0 + 1 ) = 1
111 110 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
112 nnuz 
 |-  NN = ( ZZ>= ` 1 )
113 111 112 eqtr4i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = NN
114 109 113 eleqtrrdi 
 |-  ( ph -> E e. ( ZZ>= ` ( 0 + 1 ) ) )
115 fzosplitsnm1 
 |-  ( ( 0 e. ZZ /\ E e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( 0 ..^ E ) = ( ( 0 ..^ ( E - 1 ) ) u. { ( E - 1 ) } ) )
116 106 114 115 syl2anc 
 |-  ( ph -> ( 0 ..^ E ) = ( ( 0 ..^ ( E - 1 ) ) u. { ( E - 1 ) } ) )
117 11 116 eleqtrd 
 |-  ( ph -> ( `' U ` K ) e. ( ( 0 ..^ ( E - 1 ) ) u. { ( E - 1 ) } ) )
118 fvex 
 |-  ( `' U ` K ) e. _V
119 elunsn 
 |-  ( ( `' U ` K ) e. _V -> ( ( `' U ` K ) e. ( ( 0 ..^ ( E - 1 ) ) u. { ( E - 1 ) } ) <-> ( ( `' U ` K ) e. ( 0 ..^ ( E - 1 ) ) \/ ( `' U ` K ) = ( E - 1 ) ) ) )
120 118 119 ax-mp 
 |-  ( ( `' U ` K ) e. ( ( 0 ..^ ( E - 1 ) ) u. { ( E - 1 ) } ) <-> ( ( `' U ` K ) e. ( 0 ..^ ( E - 1 ) ) \/ ( `' U ` K ) = ( E - 1 ) ) )
121 117 120 sylib 
 |-  ( ph -> ( ( `' U ` K ) e. ( 0 ..^ ( E - 1 ) ) \/ ( `' U ` K ) = ( E - 1 ) ) )
122 83 105 121 mpjaodan 
 |-  ( ph -> ( `' U ` K ) e. ( 0 ..^ ( E - 1 ) ) )
123 elfzom1elp1fzo 
 |-  ( ( E e. ZZ /\ ( `' U ` K ) e. ( 0 ..^ ( E - 1 ) ) ) -> ( ( `' U ` K ) + 1 ) e. ( 0 ..^ E ) )
124 82 122 123 syl2anc 
 |-  ( ph -> ( ( `' U ` K ) + 1 ) e. ( 0 ..^ E ) )
125 77 124 eqeltrrd 
 |-  ( ph -> ( ( `' W ` K ) + 1 ) e. ( 0 ..^ E ) )
126 18 70 41 20 125 splfv1 
 |-  ( ph -> ( ( W splice <. E , E , <" I "> >. ) ` ( ( `' W ` K ) + 1 ) ) = ( W ` ( ( `' W ` K ) + 1 ) ) )
127 81 126 eqtrd 
 |-  ( ph -> ( U ` ( ( `' W ` K ) + 1 ) ) = ( W ` ( ( `' W ` K ) + 1 ) ) )
128 1zzd 
 |-  ( ph -> 1 e. ZZ )
129 82 128 zsubcld 
 |-  ( ph -> ( E - 1 ) e. ZZ )
130 lencl 
 |-  ( W e. Word D -> ( # ` W ) e. NN0 )
131 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
132 131 biimpi 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
133 18 130 132 3syl 
 |-  ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
134 133 elfzelzd 
 |-  ( ph -> ( # ` W ) e. ZZ )
135 134 128 zsubcld 
 |-  ( ph -> ( ( # ` W ) - 1 ) e. ZZ )
136 109 nnred 
 |-  ( ph -> E e. RR )
137 134 zred 
 |-  ( ph -> ( # ` W ) e. RR )
138 1red 
 |-  ( ph -> 1 e. RR )
139 elfzle2 
 |-  ( E e. ( 0 ... ( # ` W ) ) -> E <_ ( # ` W ) )
140 41 139 syl 
 |-  ( ph -> E <_ ( # ` W ) )
141 136 137 138 140 lesub1dd 
 |-  ( ph -> ( E - 1 ) <_ ( ( # ` W ) - 1 ) )
142 eluz 
 |-  ( ( ( E - 1 ) e. ZZ /\ ( ( # ` W ) - 1 ) e. ZZ ) -> ( ( ( # ` W ) - 1 ) e. ( ZZ>= ` ( E - 1 ) ) <-> ( E - 1 ) <_ ( ( # ` W ) - 1 ) ) )
143 142 biimpar 
 |-  ( ( ( ( E - 1 ) e. ZZ /\ ( ( # ` W ) - 1 ) e. ZZ ) /\ ( E - 1 ) <_ ( ( # ` W ) - 1 ) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` ( E - 1 ) ) )
144 129 135 141 143 syl21anc 
 |-  ( ph -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` ( E - 1 ) ) )
145 fzoss2 
 |-  ( ( ( # ` W ) - 1 ) e. ( ZZ>= ` ( E - 1 ) ) -> ( 0 ..^ ( E - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
146 144 145 syl 
 |-  ( ph -> ( 0 ..^ ( E - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
147 146 122 sseldd 
 |-  ( ph -> ( `' U ` K ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
148 76 147 eqeltrrd 
 |-  ( ph -> ( `' W ` K ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
149 1 3 18 31 148 cycpmfv1 
 |-  ( ph -> ( ( M ` W ) ` ( W ` ( `' W ` K ) ) ) = ( W ` ( ( `' W ` K ) + 1 ) ) )
150 98 fveq2d 
 |-  ( ph -> ( ( M ` W ) ` ( W ` ( `' W ` K ) ) ) = ( ( M ` W ) ` K ) )
151 127 149 150 3eqtr2rd 
 |-  ( ph -> ( ( M ` W ) ` K ) = ( U ` ( ( `' W ` K ) + 1 ) ) )
152 79 151 eqtr4d 
 |-  ( ph -> ( ( M ` U ) ` K ) = ( ( M ` W ) ` K ) )