Metamath Proof Explorer

Theorem cycpmconjslem2

Description: Lemma for cycpmconjs . (Contributed by Thierry Arnoux, 14-Oct-2023)

Ref Expression
Hypotheses cycpmconjs.c 
|- C = ( M " ( `' # " { P } ) )
cycpmconjs.s 
|- S = ( SymGrp ` D )
cycpmconjs.n 
|- N = ( # ` D )
cycpmconjs.m 
|- M = ( toCyc ` D )
cycpmconjs.b 
|- B = ( Base ` S )
cycpmconjs.a 
|- .+ = ( +g ` S )
cycpmconjs.l 
|- .- = ( -g ` S )
cycpmconjs.p 
|- ( ph -> P e. ( 0 ... N ) )
cycpmconjs.d 
|- ( ph -> D e. Fin )
cycpmconjs.q 
|- ( ph -> Q e. C )
Assertion cycpmconjslem2 
|- ( ph -> E. q ( q : ( 0 ..^ N ) -1-1-onto-> D /\ ( ( `' q o. Q ) o. q ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cycpmconjs.c 
 |-  C = ( M " ( `' # " { P } ) )
2 cycpmconjs.s 
 |-  S = ( SymGrp ` D )
3 cycpmconjs.n 
 |-  N = ( # ` D )
4 cycpmconjs.m 
 |-  M = ( toCyc ` D )
5 cycpmconjs.b 
 |-  B = ( Base ` S )
6 cycpmconjs.a 
 |-  .+ = ( +g ` S )
7 cycpmconjs.l 
 |-  .- = ( -g ` S )
8 cycpmconjs.p 
 |-  ( ph -> P e. ( 0 ... N ) )
9 cycpmconjs.d 
 |-  ( ph -> D e. Fin )
10 cycpmconjs.q 
 |-  ( ph -> Q e. C )
11 fzofi 
 |-  ( 0 ..^ N ) e. Fin
12 diffi 
 |-  ( ( 0 ..^ N ) e. Fin -> ( ( 0 ..^ N ) \ dom u ) e. Fin )
13 11 12 mp1i 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( ( 0 ..^ N ) \ dom u ) e. Fin )
14 diffi 
 |-  ( D e. Fin -> ( D \ ran u ) e. Fin )
15 9 14 syl 
 |-  ( ph -> ( D \ ran u ) e. Fin )
16 15 ad2antrr 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( D \ ran u ) e. Fin )
17 hashcl 
 |-  ( D e. Fin -> ( # ` D ) e. NN0 )
18 9 17 syl 
 |-  ( ph -> ( # ` D ) e. NN0 )
19 3 18 eqeltrid 
 |-  ( ph -> N e. NN0 )
20 hashfzo0 
 |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
21 19 20 syl 
 |-  ( ph -> ( # ` ( 0 ..^ N ) ) = N )
22 21 3 eqtrdi 
 |-  ( ph -> ( # ` ( 0 ..^ N ) ) = ( # ` D ) )
23 22 ad2antrr 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` ( 0 ..^ N ) ) = ( # ` D ) )
24 simplr 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) )
25 24 elin1d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u e. { w e. Word D | w : dom w -1-1-> D } )
26 elrabi 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } -> u e. Word D )
27 wrdfin 
 |-  ( u e. Word D -> u e. Fin )
28 25 26 27 3syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u e. Fin )
29 id 
 |-  ( w = u -> w = u )
30 dmeq 
 |-  ( w = u -> dom w = dom u )
31 eqidd 
 |-  ( w = u -> D = D )
32 29 30 31 f1eq123d 
 |-  ( w = u -> ( w : dom w -1-1-> D <-> u : dom u -1-1-> D ) )
33 32 elrab 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } <-> ( u e. Word D /\ u : dom u -1-1-> D ) )
34 33 simprbi 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } -> u : dom u -1-1-> D )
35 25 34 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u : dom u -1-1-> D )
36 f1fun 
 |-  ( u : dom u -1-1-> D -> Fun u )
37 35 36 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> Fun u )
38 hashfun 
 |-  ( u e. Fin -> ( Fun u <-> ( # ` u ) = ( # ` dom u ) ) )
39 38 biimpa 
 |-  ( ( u e. Fin /\ Fun u ) -> ( # ` u ) = ( # ` dom u ) )
40 28 37 39 syl2anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) = ( # ` dom u ) )
41 24 dmexd 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> dom u e. _V )
42 hashf1rn 
 |-  ( ( dom u e. _V /\ u : dom u -1-1-> D ) -> ( # ` u ) = ( # ` ran u ) )
43 41 35 42 syl2anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) = ( # ` ran u ) )
44 40 43 eqtr3d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` dom u ) = ( # ` ran u ) )
45 23 44 oveq12d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( ( # ` ( 0 ..^ N ) ) - ( # ` dom u ) ) = ( ( # ` D ) - ( # ` ran u ) ) )
46 11 a1i 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( 0 ..^ N ) e. Fin )
47 wrddm 
 |-  ( u e. Word D -> dom u = ( 0 ..^ ( # ` u ) ) )
48 25 26 47 3syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> dom u = ( 0 ..^ ( # ` u ) ) )
49 hashcl 
 |-  ( u e. Fin -> ( # ` u ) e. NN0 )
50 25 26 27 49 4syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) e. NN0 )
51 50 nn0zd 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) e. ZZ )
52 18 nn0zd 
 |-  ( ph -> ( # ` D ) e. ZZ )
53 3 52 eqeltrid 
 |-  ( ph -> N e. ZZ )
54 53 ad2antrr 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> N e. ZZ )
55 9 ad2antrr 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> D e. Fin )
56 wrdf 
 |-  ( u e. Word D -> u : ( 0 ..^ ( # ` u ) ) --> D )
57 56 frnd 
 |-  ( u e. Word D -> ran u C_ D )
58 25 26 57 3syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ran u C_ D )
59 hashss 
 |-  ( ( D e. Fin /\ ran u C_ D ) -> ( # ` ran u ) <_ ( # ` D ) )
60 55 58 59 syl2anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` ran u ) <_ ( # ` D ) )
61 3 a1i 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> N = ( # ` D ) )
62 60 43 61 3brtr4d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) <_ N )
63 eluz1 
 |-  ( ( # ` u ) e. ZZ -> ( N e. ( ZZ>= ` ( # ` u ) ) <-> ( N e. ZZ /\ ( # ` u ) <_ N ) ) )
64 63 biimpar 
 |-  ( ( ( # ` u ) e. ZZ /\ ( N e. ZZ /\ ( # ` u ) <_ N ) ) -> N e. ( ZZ>= ` ( # ` u ) ) )
65 51 54 62 64 syl12anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> N e. ( ZZ>= ` ( # ` u ) ) )
66 fzoss2 
 |-  ( N e. ( ZZ>= ` ( # ` u ) ) -> ( 0 ..^ ( # ` u ) ) C_ ( 0 ..^ N ) )
67 65 66 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( 0 ..^ ( # ` u ) ) C_ ( 0 ..^ N ) )
68 48 67 eqsstrd 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> dom u C_ ( 0 ..^ N ) )
69 hashssdif 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ dom u C_ ( 0 ..^ N ) ) -> ( # ` ( ( 0 ..^ N ) \ dom u ) ) = ( ( # ` ( 0 ..^ N ) ) - ( # ` dom u ) ) )
70 46 68 69 syl2anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` ( ( 0 ..^ N ) \ dom u ) ) = ( ( # ` ( 0 ..^ N ) ) - ( # ` dom u ) ) )
71 hashssdif 
 |-  ( ( D e. Fin /\ ran u C_ D ) -> ( # ` ( D \ ran u ) ) = ( ( # ` D ) - ( # ` ran u ) ) )
72 55 58 71 syl2anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` ( D \ ran u ) ) = ( ( # ` D ) - ( # ` ran u ) ) )
73 45 70 72 3eqtr4d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` ( ( 0 ..^ N ) \ dom u ) ) = ( # ` ( D \ ran u ) ) )
74 hasheqf1o 
 |-  ( ( ( ( 0 ..^ N ) \ dom u ) e. Fin /\ ( D \ ran u ) e. Fin ) -> ( ( # ` ( ( 0 ..^ N ) \ dom u ) ) = ( # ` ( D \ ran u ) ) <-> E. f f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) )
75 74 biimpa 
 |-  ( ( ( ( ( 0 ..^ N ) \ dom u ) e. Fin /\ ( D \ ran u ) e. Fin ) /\ ( # ` ( ( 0 ..^ N ) \ dom u ) ) = ( # ` ( D \ ran u ) ) ) -> E. f f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) )
76 13 16 73 75 syl21anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> E. f f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) )
77 35 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> u : dom u -1-1-> D )
78 f1f1orn 
 |-  ( u : dom u -1-1-> D -> u : dom u -1-1-onto-> ran u )
79 77 78 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> u : dom u -1-1-onto-> ran u )
80 simpr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) )
81 disjdif 
 |-  ( dom u i^i ( ( 0 ..^ N ) \ dom u ) ) = (/)
82 81 a1i 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( dom u i^i ( ( 0 ..^ N ) \ dom u ) ) = (/) )
83 disjdif 
 |-  ( ran u i^i ( D \ ran u ) ) = (/)
84 83 a1i 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ran u i^i ( D \ ran u ) ) = (/) )
85 f1oun 
 |-  ( ( ( u : dom u -1-1-onto-> ran u /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) /\ ( ( dom u i^i ( ( 0 ..^ N ) \ dom u ) ) = (/) /\ ( ran u i^i ( D \ ran u ) ) = (/) ) ) -> ( u u. f ) : ( dom u u. ( ( 0 ..^ N ) \ dom u ) ) -1-1-onto-> ( ran u u. ( D \ ran u ) ) )
86 79 80 82 84 85 syl22anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( u u. f ) : ( dom u u. ( ( 0 ..^ N ) \ dom u ) ) -1-1-onto-> ( ran u u. ( D \ ran u ) ) )
87 eqidd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( u u. f ) = ( u u. f ) )
88 68 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> dom u C_ ( 0 ..^ N ) )
89 undif 
 |-  ( dom u C_ ( 0 ..^ N ) <-> ( dom u u. ( ( 0 ..^ N ) \ dom u ) ) = ( 0 ..^ N ) )
90 88 89 sylib 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( dom u u. ( ( 0 ..^ N ) \ dom u ) ) = ( 0 ..^ N ) )
91 undif 
 |-  ( ran u C_ D <-> ( ran u u. ( D \ ran u ) ) = D )
92 58 91 sylib 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( ran u u. ( D \ ran u ) ) = D )
93 92 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ran u u. ( D \ ran u ) ) = D )
94 87 90 93 f1oeq123d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( u u. f ) : ( dom u u. ( ( 0 ..^ N ) \ dom u ) ) -1-1-onto-> ( ran u u. ( D \ ran u ) ) <-> ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D ) )
95 86 94 mpbid 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D )
96 f1ocnv 
 |-  ( ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D -> `' ( u u. f ) : D -1-1-onto-> ( 0 ..^ N ) )
97 95 96 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> `' ( u u. f ) : D -1-1-onto-> ( 0 ..^ N ) )
98 1 2 3 4 5 cycpmgcl 
 |-  ( ( D e. Fin /\ P e. ( 0 ... N ) ) -> C C_ B )
99 9 8 98 syl2anc 
 |-  ( ph -> C C_ B )
100 99 10 sseldd 
 |-  ( ph -> Q e. B )
101 2 5 symgbasf1o 
 |-  ( Q e. B -> Q : D -1-1-onto-> D )
102 100 101 syl 
 |-  ( ph -> Q : D -1-1-onto-> D )
103 102 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> Q : D -1-1-onto-> D )
104 f1oco 
 |-  ( ( `' ( u u. f ) : D -1-1-onto-> ( 0 ..^ N ) /\ Q : D -1-1-onto-> D ) -> ( `' ( u u. f ) o. Q ) : D -1-1-onto-> ( 0 ..^ N ) )
105 97 103 104 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( `' ( u u. f ) o. Q ) : D -1-1-onto-> ( 0 ..^ N ) )
106 f1oco 
 |-  ( ( ( `' ( u u. f ) o. Q ) : D -1-1-onto-> ( 0 ..^ N ) /\ ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D ) -> ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
107 105 95 106 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
108 f1ofun 
 |-  ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) -> Fun ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) )
109 funrel 
 |-  ( Fun ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) -> Rel ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) )
110 107 108 109 3syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> Rel ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) )
111 f1odm 
 |-  ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) -> dom ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( 0 ..^ N ) )
112 107 111 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> dom ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( 0 ..^ N ) )
113 fzosplit 
 |-  ( P e. ( 0 ... N ) -> ( 0 ..^ N ) = ( ( 0 ..^ P ) u. ( P ..^ N ) ) )
114 8 113 syl 
 |-  ( ph -> ( 0 ..^ N ) = ( ( 0 ..^ P ) u. ( P ..^ N ) ) )
115 114 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( 0 ..^ N ) = ( ( 0 ..^ P ) u. ( P ..^ N ) ) )
116 112 115 eqtrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> dom ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( 0 ..^ P ) u. ( P ..^ N ) ) )
117 fzodisj 
 |-  ( ( 0 ..^ P ) i^i ( P ..^ N ) ) = (/)
118 reldisjun 
 |-  ( ( Rel ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) /\ dom ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( 0 ..^ P ) u. ( P ..^ N ) ) /\ ( ( 0 ..^ P ) i^i ( P ..^ N ) ) = (/) ) -> ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( 0 ..^ P ) ) u. ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( P ..^ N ) ) ) )
119 117 118 mp3an3 
 |-  ( ( Rel ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) /\ dom ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( 0 ..^ P ) u. ( P ..^ N ) ) ) -> ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( 0 ..^ P ) ) u. ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( P ..^ N ) ) ) )
120 110 116 119 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( 0 ..^ P ) ) u. ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( P ..^ N ) ) ) )
121 resco 
 |-  ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( 0 ..^ P ) ) = ( ( `' ( u u. f ) o. Q ) o. ( ( u u. f ) |` ( 0 ..^ P ) ) )
122 121 a1i 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( 0 ..^ P ) ) = ( ( `' ( u u. f ) o. Q ) o. ( ( u u. f ) |` ( 0 ..^ P ) ) ) )
123 25 26 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u e. Word D )
124 wrdfn 
 |-  ( u e. Word D -> u Fn ( 0 ..^ ( # ` u ) ) )
125 123 124 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u Fn ( 0 ..^ ( # ` u ) ) )
126 24 elin2d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u e. ( `' # " { P } ) )
127 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
128 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
129 fniniseg 
 |-  ( # Fn _V -> ( u e. ( `' # " { P } ) <-> ( u e. _V /\ ( # ` u ) = P ) ) )
130 127 128 129 mp2b 
 |-  ( u e. ( `' # " { P } ) <-> ( u e. _V /\ ( # ` u ) = P ) )
131 130 simprbi 
 |-  ( u e. ( `' # " { P } ) -> ( # ` u ) = P )
132 126 131 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) = P )
133 132 oveq2d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( 0 ..^ ( # ` u ) ) = ( 0 ..^ P ) )
134 133 fneq2d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( u Fn ( 0 ..^ ( # ` u ) ) <-> u Fn ( 0 ..^ P ) ) )
135 125 134 mpbid 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u Fn ( 0 ..^ P ) )
136 135 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> u Fn ( 0 ..^ P ) )
137 f1ofn 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) -> f Fn ( ( 0 ..^ N ) \ dom u ) )
138 80 137 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> f Fn ( ( 0 ..^ N ) \ dom u ) )
139 48 133 eqtrd 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> dom u = ( 0 ..^ P ) )
140 139 ineq1d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( dom u i^i ( ( 0 ..^ N ) \ dom u ) ) = ( ( 0 ..^ P ) i^i ( ( 0 ..^ N ) \ dom u ) ) )
141 81 a1i 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( dom u i^i ( ( 0 ..^ N ) \ dom u ) ) = (/) )
142 140 141 eqtr3d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( ( 0 ..^ P ) i^i ( ( 0 ..^ N ) \ dom u ) ) = (/) )
143 142 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( 0 ..^ P ) i^i ( ( 0 ..^ N ) \ dom u ) ) = (/) )
144 fnunres1 
 |-  ( ( u Fn ( 0 ..^ P ) /\ f Fn ( ( 0 ..^ N ) \ dom u ) /\ ( ( 0 ..^ P ) i^i ( ( 0 ..^ N ) \ dom u ) ) = (/) ) -> ( ( u u. f ) |` ( 0 ..^ P ) ) = u )
145 136 138 143 144 syl3anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( u u. f ) |` ( 0 ..^ P ) ) = u )
146 145 coeq2d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) o. Q ) o. ( ( u u. f ) |` ( 0 ..^ P ) ) ) = ( ( `' ( u u. f ) o. Q ) o. u ) )
147 resco 
 |-  ( ( `' ( u u. f ) o. Q ) |` ran u ) = ( `' ( u u. f ) o. ( Q |` ran u ) )
148 resco 
 |-  ( ( `' u o. ( M ` u ) ) |` ran u ) = ( `' u o. ( ( M ` u ) |` ran u ) )
149 148 a1i 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' u o. ( M ` u ) ) |` ran u ) = ( `' u o. ( ( M ` u ) |` ran u ) ) )
150 cnvun 
 |-  `' ( u u. f ) = ( `' u u. `' f )
151 150 reseq1i 
 |-  ( `' ( u u. f ) |` ran u ) = ( ( `' u u. `' f ) |` ran u )
152 f1ocnv 
 |-  ( u : dom u -1-1-onto-> ran u -> `' u : ran u -1-1-onto-> dom u )
153 f1ofn 
 |-  ( `' u : ran u -1-1-onto-> dom u -> `' u Fn ran u )
154 79 152 153 3syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> `' u Fn ran u )
155 f1ocnv 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) -> `' f : ( D \ ran u ) -1-1-onto-> ( ( 0 ..^ N ) \ dom u ) )
156 f1ofn 
 |-  ( `' f : ( D \ ran u ) -1-1-onto-> ( ( 0 ..^ N ) \ dom u ) -> `' f Fn ( D \ ran u ) )
157 80 155 156 3syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> `' f Fn ( D \ ran u ) )
158 fnunres1 
 |-  ( ( `' u Fn ran u /\ `' f Fn ( D \ ran u ) /\ ( ran u i^i ( D \ ran u ) ) = (/) ) -> ( ( `' u u. `' f ) |` ran u ) = `' u )
159 154 157 84 158 syl3anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' u u. `' f ) |` ran u ) = `' u )
160 151 159 eqtr2id 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> `' u = ( `' ( u u. f ) |` ran u ) )
161 simplr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( M ` u ) = Q )
162 161 reseq1d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( M ` u ) |` ran u ) = ( Q |` ran u ) )
163 160 162 coeq12d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( `' u o. ( ( M ` u ) |` ran u ) ) = ( ( `' ( u u. f ) |` ran u ) o. ( Q |` ran u ) ) )
164 55 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> D e. Fin )
165 123 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> u e. Word D )
166 4 164 165 77 tocycfvres1 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( M ` u ) |` ran u ) = ( ( u cyclShift 1 ) o. `' u ) )
167 162 166 eqtr3d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( Q |` ran u ) = ( ( u cyclShift 1 ) o. `' u ) )
168 167 rneqd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ran ( Q |` ran u ) = ran ( ( u cyclShift 1 ) o. `' u ) )
169 1zzd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> 1 e. ZZ )
170 cshf1o 
 |-  ( ( u e. Word D /\ u : dom u -1-1-> D /\ 1 e. ZZ ) -> ( u cyclShift 1 ) : dom u -1-1-onto-> ran u )
171 165 77 169 170 syl3anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( u cyclShift 1 ) : dom u -1-1-onto-> ran u )
172 79 152 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> `' u : ran u -1-1-onto-> dom u )
173 f1oco 
 |-  ( ( ( u cyclShift 1 ) : dom u -1-1-onto-> ran u /\ `' u : ran u -1-1-onto-> dom u ) -> ( ( u cyclShift 1 ) o. `' u ) : ran u -1-1-onto-> ran u )
174 171 172 173 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( u cyclShift 1 ) o. `' u ) : ran u -1-1-onto-> ran u )
175 f1ofo 
 |-  ( ( ( u cyclShift 1 ) o. `' u ) : ran u -1-1-onto-> ran u -> ( ( u cyclShift 1 ) o. `' u ) : ran u -onto-> ran u )
176 forn 
 |-  ( ( ( u cyclShift 1 ) o. `' u ) : ran u -onto-> ran u -> ran ( ( u cyclShift 1 ) o. `' u ) = ran u )
177 174 175 176 3syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ran ( ( u cyclShift 1 ) o. `' u ) = ran u )
178 168 177 eqtrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ran ( Q |` ran u ) = ran u )
179 ssid 
 |-  ran u C_ ran u
180 178 179 eqsstrdi 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ran ( Q |` ran u ) C_ ran u )
181 cores 
 |-  ( ran ( Q |` ran u ) C_ ran u -> ( ( `' ( u u. f ) |` ran u ) o. ( Q |` ran u ) ) = ( `' ( u u. f ) o. ( Q |` ran u ) ) )
182 180 181 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) |` ran u ) o. ( Q |` ran u ) ) = ( `' ( u u. f ) o. ( Q |` ran u ) ) )
183 149 163 182 3eqtrrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( `' ( u u. f ) o. ( Q |` ran u ) ) = ( ( `' u o. ( M ` u ) ) |` ran u ) )
184 147 183 syl5eq 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) o. Q ) |` ran u ) = ( ( `' u o. ( M ` u ) ) |` ran u ) )
185 184 coeq1d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' ( u u. f ) o. Q ) |` ran u ) o. u ) = ( ( ( `' u o. ( M ` u ) ) |` ran u ) o. u ) )
186 cores 
 |-  ( ran u C_ ran u -> ( ( ( `' u o. ( M ` u ) ) |` ran u ) o. u ) = ( ( `' u o. ( M ` u ) ) o. u ) )
187 179 186 mp1i 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' u o. ( M ` u ) ) |` ran u ) o. u ) = ( ( `' u o. ( M ` u ) ) o. u ) )
188 185 187 eqtrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' ( u u. f ) o. Q ) |` ran u ) o. u ) = ( ( `' u o. ( M ` u ) ) o. u ) )
189 cores 
 |-  ( ran u C_ ran u -> ( ( ( `' ( u u. f ) o. Q ) |` ran u ) o. u ) = ( ( `' ( u u. f ) o. Q ) o. u ) )
190 179 189 mp1i 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' ( u u. f ) o. Q ) |` ran u ) o. u ) = ( ( `' ( u u. f ) o. Q ) o. u ) )
191 132 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( # ` u ) = P )
192 1 2 3 4 164 165 77 191 cycpmconjslem1 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' u o. ( M ` u ) ) o. u ) = ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) )
193 188 190 192 3eqtr3d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) o. Q ) o. u ) = ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) )
194 122 146 193 3eqtrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( 0 ..^ P ) ) = ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) )
195 resco 
 |-  ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( P ..^ N ) ) = ( ( `' ( u u. f ) o. Q ) o. ( ( u u. f ) |` ( P ..^ N ) ) )
196 139 adantr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> dom u = ( 0 ..^ P ) )
197 196 difeq2d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( 0 ..^ N ) \ dom u ) = ( ( 0 ..^ N ) \ ( 0 ..^ P ) ) )
198 fzodif1 
 |-  ( P e. ( 0 ... N ) -> ( ( 0 ..^ N ) \ ( 0 ..^ P ) ) = ( P ..^ N ) )
199 8 198 syl 
 |-  ( ph -> ( ( 0 ..^ N ) \ ( 0 ..^ P ) ) = ( P ..^ N ) )
200 199 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( 0 ..^ N ) \ ( 0 ..^ P ) ) = ( P ..^ N ) )
201 197 200 eqtrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( 0 ..^ N ) \ dom u ) = ( P ..^ N ) )
202 201 reseq2d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( u u. f ) |` ( ( 0 ..^ N ) \ dom u ) ) = ( ( u u. f ) |` ( P ..^ N ) ) )
203 fnunres2 
 |-  ( ( u Fn ( 0 ..^ P ) /\ f Fn ( ( 0 ..^ N ) \ dom u ) /\ ( ( 0 ..^ P ) i^i ( ( 0 ..^ N ) \ dom u ) ) = (/) ) -> ( ( u u. f ) |` ( ( 0 ..^ N ) \ dom u ) ) = f )
204 136 138 143 203 syl3anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( u u. f ) |` ( ( 0 ..^ N ) \ dom u ) ) = f )
205 202 204 eqtr3d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( u u. f ) |` ( P ..^ N ) ) = f )
206 205 coeq2d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) o. Q ) o. ( ( u u. f ) |` ( P ..^ N ) ) ) = ( ( `' ( u u. f ) o. Q ) o. f ) )
207 195 206 syl5eq 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( P ..^ N ) ) = ( ( `' ( u u. f ) o. Q ) o. f ) )
208 150 reseq1i 
 |-  ( `' ( u u. f ) |` ( D \ ran u ) ) = ( ( `' u u. `' f ) |` ( D \ ran u ) )
209 fnunres2 
 |-  ( ( `' u Fn ran u /\ `' f Fn ( D \ ran u ) /\ ( ran u i^i ( D \ ran u ) ) = (/) ) -> ( ( `' u u. `' f ) |` ( D \ ran u ) ) = `' f )
210 154 157 84 209 syl3anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' u u. `' f ) |` ( D \ ran u ) ) = `' f )
211 208 210 syl5eq 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( `' ( u u. f ) |` ( D \ ran u ) ) = `' f )
212 161 reseq1d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( M ` u ) |` ( D \ ran u ) ) = ( Q |` ( D \ ran u ) ) )
213 4 164 165 77 tocycfvres2 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( M ` u ) |` ( D \ ran u ) ) = ( _I |` ( D \ ran u ) ) )
214 212 213 eqtr3d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( Q |` ( D \ ran u ) ) = ( _I |` ( D \ ran u ) ) )
215 211 214 coeq12d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) |` ( D \ ran u ) ) o. ( Q |` ( D \ ran u ) ) ) = ( `' f o. ( _I |` ( D \ ran u ) ) ) )
216 214 rneqd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ran ( Q |` ( D \ ran u ) ) = ran ( _I |` ( D \ ran u ) ) )
217 rnresi 
 |-  ran ( _I |` ( D \ ran u ) ) = ( D \ ran u )
218 217 eqimssi 
 |-  ran ( _I |` ( D \ ran u ) ) C_ ( D \ ran u )
219 216 218 eqsstrdi 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ran ( Q |` ( D \ ran u ) ) C_ ( D \ ran u ) )
220 cores 
 |-  ( ran ( Q |` ( D \ ran u ) ) C_ ( D \ ran u ) -> ( ( `' ( u u. f ) |` ( D \ ran u ) ) o. ( Q |` ( D \ ran u ) ) ) = ( `' ( u u. f ) o. ( Q |` ( D \ ran u ) ) ) )
221 219 220 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) |` ( D \ ran u ) ) o. ( Q |` ( D \ ran u ) ) ) = ( `' ( u u. f ) o. ( Q |` ( D \ ran u ) ) ) )
222 resco 
 |-  ( ( `' ( u u. f ) o. Q ) |` ( D \ ran u ) ) = ( `' ( u u. f ) o. ( Q |` ( D \ ran u ) ) )
223 221 222 eqtr4di 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) |` ( D \ ran u ) ) o. ( Q |` ( D \ ran u ) ) ) = ( ( `' ( u u. f ) o. Q ) |` ( D \ ran u ) ) )
224 215 223 eqtr3d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( `' f o. ( _I |` ( D \ ran u ) ) ) = ( ( `' ( u u. f ) o. Q ) |` ( D \ ran u ) ) )
225 224 coeq1d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' f o. ( _I |` ( D \ ran u ) ) ) o. f ) = ( ( ( `' ( u u. f ) o. Q ) |` ( D \ ran u ) ) o. f ) )
226 f1of 
 |-  ( `' f : ( D \ ran u ) -1-1-onto-> ( ( 0 ..^ N ) \ dom u ) -> `' f : ( D \ ran u ) --> ( ( 0 ..^ N ) \ dom u ) )
227 80 155 226 3syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> `' f : ( D \ ran u ) --> ( ( 0 ..^ N ) \ dom u ) )
228 fcoi1 
 |-  ( `' f : ( D \ ran u ) --> ( ( 0 ..^ N ) \ dom u ) -> ( `' f o. ( _I |` ( D \ ran u ) ) ) = `' f )
229 227 228 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( `' f o. ( _I |` ( D \ ran u ) ) ) = `' f )
230 229 coeq1d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' f o. ( _I |` ( D \ ran u ) ) ) o. f ) = ( `' f o. f ) )
231 f1ococnv1 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) -> ( `' f o. f ) = ( _I |` ( ( 0 ..^ N ) \ dom u ) ) )
232 80 231 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( `' f o. f ) = ( _I |` ( ( 0 ..^ N ) \ dom u ) ) )
233 201 reseq2d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( _I |` ( ( 0 ..^ N ) \ dom u ) ) = ( _I |` ( P ..^ N ) ) )
234 230 232 233 3eqtrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' f o. ( _I |` ( D \ ran u ) ) ) o. f ) = ( _I |` ( P ..^ N ) ) )
235 f1of 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) -> f : ( ( 0 ..^ N ) \ dom u ) --> ( D \ ran u ) )
236 frn 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) --> ( D \ ran u ) -> ran f C_ ( D \ ran u ) )
237 80 235 236 3syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ran f C_ ( D \ ran u ) )
238 cores 
 |-  ( ran f C_ ( D \ ran u ) -> ( ( ( `' ( u u. f ) o. Q ) |` ( D \ ran u ) ) o. f ) = ( ( `' ( u u. f ) o. Q ) o. f ) )
239 237 238 syl 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' ( u u. f ) o. Q ) |` ( D \ ran u ) ) o. f ) = ( ( `' ( u u. f ) o. Q ) o. f ) )
240 225 234 239 3eqtr3rd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) o. Q ) o. f ) = ( _I |` ( P ..^ N ) ) )
241 207 240 eqtrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( P ..^ N ) ) = ( _I |` ( P ..^ N ) ) )
242 194 241 uneq12d 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( 0 ..^ P ) ) u. ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( P ..^ N ) ) ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) )
243 120 242 eqtrd 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) )
244 vex 
 |-  u e. _V
245 vex 
 |-  f e. _V
246 244 245 unex 
 |-  ( u u. f ) e. _V
247 f1oeq1 
 |-  ( q = ( u u. f ) -> ( q : ( 0 ..^ N ) -1-1-onto-> D <-> ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D ) )
248 cnveq 
 |-  ( q = ( u u. f ) -> `' q = `' ( u u. f ) )
249 248 coeq1d 
 |-  ( q = ( u u. f ) -> ( `' q o. Q ) = ( `' ( u u. f ) o. Q ) )
250 id 
 |-  ( q = ( u u. f ) -> q = ( u u. f ) )
251 249 250 coeq12d 
 |-  ( q = ( u u. f ) -> ( ( `' q o. Q ) o. q ) = ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) )
252 251 eqeq1d 
 |-  ( q = ( u u. f ) -> ( ( ( `' q o. Q ) o. q ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) <-> ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) )
253 247 252 anbi12d 
 |-  ( q = ( u u. f ) -> ( ( q : ( 0 ..^ N ) -1-1-onto-> D /\ ( ( `' q o. Q ) o. q ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) <-> ( ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D /\ ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) ) )
254 246 253 spcev 
 |-  ( ( ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D /\ ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) -> E. q ( q : ( 0 ..^ N ) -1-1-onto-> D /\ ( ( `' q o. Q ) o. q ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) )
255 95 243 254 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) /\ f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) ) -> E. q ( q : ( 0 ..^ N ) -1-1-onto-> D /\ ( ( `' q o. Q ) o. q ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) )
256 76 255 exlimddv 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> E. q ( q : ( 0 ..^ N ) -1-1-onto-> D /\ ( ( `' q o. Q ) o. q ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) )
257 nfcv 
 |-  F/_ u M
258 4 2 5 tocycf 
 |-  ( D e. Fin -> M : { w e. Word D | w : dom w -1-1-> D } --> B )
259 ffn 
 |-  ( M : { w e. Word D | w : dom w -1-1-> D } --> B -> M Fn { w e. Word D | w : dom w -1-1-> D } )
260 9 258 259 3syl 
 |-  ( ph -> M Fn { w e. Word D | w : dom w -1-1-> D } )
261 10 1 eleqtrdi 
 |-  ( ph -> Q e. ( M " ( `' # " { P } ) ) )
262 257 260 261 fvelimad 
 |-  ( ph -> E. u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ( M ` u ) = Q )
263 256 262 r19.29a 
 |-  ( ph -> E. q ( q : ( 0 ..^ N ) -1-1-onto-> D /\ ( ( `' q o. Q ) o. q ) = ( ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) u. ( _I |` ( P ..^ N ) ) ) ) )