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 25 elrabrd 
 |-  ( ( ( 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 )
34 f1fun 
 |-  ( u : dom u -1-1-> D -> Fun u )
35 33 34 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> Fun u )
36 hashfundm 
 |-  ( ( u e. Fin /\ Fun u ) -> ( # ` u ) = ( # ` dom u ) )
37 28 35 36 syl2anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) = ( # ` dom u ) )
38 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 )
39 hashf1rn 
 |-  ( ( dom u e. _V /\ u : dom u -1-1-> D ) -> ( # ` u ) = ( # ` ran u ) )
40 38 33 39 syl2anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) = ( # ` ran u ) )
41 37 40 eqtr3d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` dom u ) = ( # ` ran u ) )
42 23 41 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 ) ) )
43 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 )
44 wrddm 
 |-  ( u e. Word D -> dom u = ( 0 ..^ ( # ` u ) ) )
45 25 26 44 3syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> dom u = ( 0 ..^ ( # ` u ) ) )
46 hashcl 
 |-  ( u e. Fin -> ( # ` u ) e. NN0 )
47 25 26 27 46 4syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) e. NN0 )
48 47 nn0zd 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) e. ZZ )
49 18 nn0zd 
 |-  ( ph -> ( # ` D ) e. ZZ )
50 3 49 eqeltrid 
 |-  ( ph -> N e. ZZ )
51 50 ad2antrr 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> N e. ZZ )
52 9 ad2antrr 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> D e. Fin )
53 wrdf 
 |-  ( u e. Word D -> u : ( 0 ..^ ( # ` u ) ) --> D )
54 53 frnd 
 |-  ( u e. Word D -> ran u C_ D )
55 25 26 54 3syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ran u C_ D )
56 hashss 
 |-  ( ( D e. Fin /\ ran u C_ D ) -> ( # ` ran u ) <_ ( # ` D ) )
57 52 55 56 syl2anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` ran u ) <_ ( # ` D ) )
58 3 a1i 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> N = ( # ` D ) )
59 57 40 58 3brtr4d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) <_ N )
60 eluz1 
 |-  ( ( # ` u ) e. ZZ -> ( N e. ( ZZ>= ` ( # ` u ) ) <-> ( N e. ZZ /\ ( # ` u ) <_ N ) ) )
61 60 biimpar 
 |-  ( ( ( # ` u ) e. ZZ /\ ( N e. ZZ /\ ( # ` u ) <_ N ) ) -> N e. ( ZZ>= ` ( # ` u ) ) )
62 48 51 59 61 syl12anc 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> N e. ( ZZ>= ` ( # ` u ) ) )
63 fzoss2 
 |-  ( N e. ( ZZ>= ` ( # ` u ) ) -> ( 0 ..^ ( # ` u ) ) C_ ( 0 ..^ N ) )
64 62 63 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 ) )
65 45 64 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 ) )
66 hashssdif 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ dom u C_ ( 0 ..^ N ) ) -> ( # ` ( ( 0 ..^ N ) \ dom u ) ) = ( ( # ` ( 0 ..^ N ) ) - ( # ` dom u ) ) )
67 43 65 66 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 ) ) )
68 hashssdif 
 |-  ( ( D e. Fin /\ ran u C_ D ) -> ( # ` ( D \ ran u ) ) = ( ( # ` D ) - ( # ` ran u ) ) )
69 52 55 68 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 ) ) )
70 42 67 69 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 ) ) )
71 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 ) ) )
72 71 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 ) )
73 13 16 70 72 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 ) )
74 33 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 )
75 f1f1orn 
 |-  ( u : dom u -1-1-> D -> u : dom u -1-1-onto-> ran u )
76 74 75 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 )
77 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 ) )
78 disjdif 
 |-  ( dom u i^i ( ( 0 ..^ N ) \ dom u ) ) = (/)
79 78 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 ) ) = (/) )
80 disjdif 
 |-  ( ran u i^i ( D \ ran u ) ) = (/)
81 80 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 ) ) = (/) )
82 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 ) ) )
83 76 77 79 81 82 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 ) ) )
84 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 ) )
85 65 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 ) )
86 undif 
 |-  ( dom u C_ ( 0 ..^ N ) <-> ( dom u u. ( ( 0 ..^ N ) \ dom u ) ) = ( 0 ..^ N ) )
87 85 86 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 ) )
88 undif 
 |-  ( ran u C_ D <-> ( ran u u. ( D \ ran u ) ) = D )
89 55 88 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 )
90 89 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 )
91 84 87 90 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 ) )
92 83 91 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 )
93 f1ocnv 
 |-  ( ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D -> `' ( u u. f ) : D -1-1-onto-> ( 0 ..^ N ) )
94 92 93 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 ) )
95 1 2 3 4 5 cycpmgcl 
 |-  ( ( D e. Fin /\ P e. ( 0 ... N ) ) -> C C_ B )
96 9 8 95 syl2anc 
 |-  ( ph -> C C_ B )
97 96 10 sseldd 
 |-  ( ph -> Q e. B )
98 2 5 symgbasf1o 
 |-  ( Q e. B -> Q : D -1-1-onto-> D )
99 97 98 syl 
 |-  ( ph -> Q : D -1-1-onto-> D )
100 99 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 )
101 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 ) )
102 94 100 101 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 ) )
103 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 ) )
104 102 92 103 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 ) )
105 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 ) ) )
106 funrel 
 |-  ( Fun ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) -> Rel ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) )
107 104 105 106 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 ) ) )
108 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 ) )
109 104 108 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 ) )
110 fzosplit 
 |-  ( P e. ( 0 ... N ) -> ( 0 ..^ N ) = ( ( 0 ..^ P ) u. ( P ..^ N ) ) )
111 8 110 syl 
 |-  ( ph -> ( 0 ..^ N ) = ( ( 0 ..^ P ) u. ( P ..^ N ) ) )
112 111 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 ) ) )
113 109 112 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 ) ) )
114 reldmun 
 |-  ( ( 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 ) ) ) )
115 107 113 114 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 ) ) ) )
116 resco 
 |-  ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( 0 ..^ P ) ) = ( ( `' ( u u. f ) o. Q ) o. ( ( u u. f ) |` ( 0 ..^ P ) ) )
117 116 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 ) ) ) )
118 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 )
119 wrdfn 
 |-  ( u e. Word D -> u Fn ( 0 ..^ ( # ` u ) ) )
120 118 119 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u Fn ( 0 ..^ ( # ` u ) ) )
121 24 elin2d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u e. ( `' # " { P } ) )
122 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
123 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
124 fniniseg 
 |-  ( # Fn _V -> ( u e. ( `' # " { P } ) <-> ( u e. _V /\ ( # ` u ) = P ) ) )
125 122 123 124 mp2b 
 |-  ( u e. ( `' # " { P } ) <-> ( u e. _V /\ ( # ` u ) = P ) )
126 125 simprbi 
 |-  ( u e. ( `' # " { P } ) -> ( # ` u ) = P )
127 121 126 syl 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( # ` u ) = P )
128 127 oveq2d 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> ( 0 ..^ ( # ` u ) ) = ( 0 ..^ P ) )
129 128 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 ) ) )
130 120 129 mpbid 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> u Fn ( 0 ..^ P ) )
131 130 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 ) )
132 f1ofn 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) -> f Fn ( ( 0 ..^ N ) \ dom u ) )
133 77 132 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 ) )
134 45 128 eqtrd 
 |-  ( ( ( ph /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = Q ) -> dom u = ( 0 ..^ P ) )
135 134 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 ) ) )
136 78 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 ) ) = (/) )
137 135 136 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 ) ) = (/) )
138 137 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 ) ) = (/) )
139 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 )
140 131 133 138 139 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 )
141 140 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 ) )
142 resco 
 |-  ( ( `' ( u u. f ) o. Q ) |` ran u ) = ( `' ( u u. f ) o. ( Q |` ran u ) )
143 resco 
 |-  ( ( `' u o. ( M ` u ) ) |` ran u ) = ( `' u o. ( ( M ` u ) |` ran u ) )
144 143 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 ) ) )
145 cnvun 
 |-  `' ( u u. f ) = ( `' u u. `' f )
146 145 reseq1i 
 |-  ( `' ( u u. f ) |` ran u ) = ( ( `' u u. `' f ) |` ran u )
147 f1ocnv 
 |-  ( u : dom u -1-1-onto-> ran u -> `' u : ran u -1-1-onto-> dom u )
148 f1ofn 
 |-  ( `' u : ran u -1-1-onto-> dom u -> `' u Fn ran u )
149 74 75 147 148 4syl 
 |-  ( ( ( ( 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 )
150 f1ocnv 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) -> `' f : ( D \ ran u ) -1-1-onto-> ( ( 0 ..^ N ) \ dom u ) )
151 f1ofn 
 |-  ( `' f : ( D \ ran u ) -1-1-onto-> ( ( 0 ..^ N ) \ dom u ) -> `' f Fn ( D \ ran u ) )
152 77 150 151 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 ) )
153 fnunres1 
 |-  ( ( `' u Fn ran u /\ `' f Fn ( D \ ran u ) /\ ( ran u i^i ( D \ ran u ) ) = (/) ) -> ( ( `' u u. `' f ) |` ran u ) = `' u )
154 149 152 81 153 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 )
155 146 154 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 ) )
156 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 )
157 156 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 ) )
158 155 157 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 ) ) )
159 52 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 )
160 118 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 )
161 4 159 160 74 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 ) )
162 157 161 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 ) )
163 162 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 ) )
164 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 )
165 cshf1o 
 |-  ( ( u e. Word D /\ u : dom u -1-1-> D /\ 1 e. ZZ ) -> ( u cyclShift 1 ) : dom u -1-1-onto-> ran u )
166 160 74 164 165 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 )
167 76 147 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 )
168 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 )
169 166 167 168 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 )
170 f1ofo 
 |-  ( ( ( u cyclShift 1 ) o. `' u ) : ran u -1-1-onto-> ran u -> ( ( u cyclShift 1 ) o. `' u ) : ran u -onto-> ran u )
171 forn 
 |-  ( ( ( u cyclShift 1 ) o. `' u ) : ran u -onto-> ran u -> ran ( ( u cyclShift 1 ) o. `' u ) = ran u )
172 169 170 171 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 )
173 163 172 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 )
174 ssid 
 |-  ran u C_ ran u
175 173 174 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 )
176 cores 
 |-  ( ran ( Q |` ran u ) C_ ran u -> ( ( `' ( u u. f ) |` ran u ) o. ( Q |` ran u ) ) = ( `' ( u u. f ) o. ( Q |` ran u ) ) )
177 175 176 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 ) ) )
178 144 158 177 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 ) )
179 142 178 eqtrid 
 |-  ( ( ( ( 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 ) )
180 179 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 ) )
181 cores 
 |-  ( ran u C_ ran u -> ( ( ( `' u o. ( M ` u ) ) |` ran u ) o. u ) = ( ( `' u o. ( M ` u ) ) o. u ) )
182 174 181 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 ) )
183 180 182 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 ) )
184 cores 
 |-  ( ran u C_ ran u -> ( ( ( `' ( u u. f ) o. Q ) |` ran u ) o. u ) = ( ( `' ( u u. f ) o. Q ) o. u ) )
185 174 184 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 ) )
186 127 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 )
187 1 2 3 4 159 160 74 186 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 ) )
188 183 185 187 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 ) )
189 117 141 188 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 ) )
190 resco 
 |-  ( ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) |` ( P ..^ N ) ) = ( ( `' ( u u. f ) o. Q ) o. ( ( u u. f ) |` ( P ..^ N ) ) )
191 134 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 ) )
192 191 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 ) ) )
193 fzodif1 
 |-  ( P e. ( 0 ... N ) -> ( ( 0 ..^ N ) \ ( 0 ..^ P ) ) = ( P ..^ N ) )
194 8 193 syl 
 |-  ( ph -> ( ( 0 ..^ N ) \ ( 0 ..^ P ) ) = ( P ..^ N ) )
195 194 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 ) )
196 192 195 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 ) )
197 196 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 ) ) )
198 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 )
199 131 133 138 198 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 )
200 197 199 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 )
201 200 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 ) )
202 190 201 eqtrid 
 |-  ( ( ( ( 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 ) )
203 145 reseq1i 
 |-  ( `' ( u u. f ) |` ( D \ ran u ) ) = ( ( `' u u. `' f ) |` ( D \ ran u ) )
204 fnunres2 
 |-  ( ( `' u Fn ran u /\ `' f Fn ( D \ ran u ) /\ ( ran u i^i ( D \ ran u ) ) = (/) ) -> ( ( `' u u. `' f ) |` ( D \ ran u ) ) = `' f )
205 149 152 81 204 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 )
206 203 205 eqtrid 
 |-  ( ( ( ( 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 )
207 156 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 ) ) )
208 4 159 160 74 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 ) ) )
209 207 208 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 ) ) )
210 206 209 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 ) ) ) )
211 209 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 ) ) )
212 rnresi 
 |-  ran ( _I |` ( D \ ran u ) ) = ( D \ ran u )
213 212 eqimssi 
 |-  ran ( _I |` ( D \ ran u ) ) C_ ( D \ ran u )
214 211 213 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 ) )
215 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 ) ) ) )
216 214 215 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 ) ) ) )
217 resco 
 |-  ( ( `' ( u u. f ) o. Q ) |` ( D \ ran u ) ) = ( `' ( u u. f ) o. ( Q |` ( D \ ran u ) ) )
218 216 217 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 ) ) )
219 210 218 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 ) ) )
220 219 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 ) )
221 f1of 
 |-  ( `' f : ( D \ ran u ) -1-1-onto-> ( ( 0 ..^ N ) \ dom u ) -> `' f : ( D \ ran u ) --> ( ( 0 ..^ N ) \ dom u ) )
222 fcoi1 
 |-  ( `' f : ( D \ ran u ) --> ( ( 0 ..^ N ) \ dom u ) -> ( `' f o. ( _I |` ( D \ ran u ) ) ) = `' f )
223 77 150 221 222 4syl 
 |-  ( ( ( ( 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 )
224 223 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 ) )
225 f1ococnv1 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) -> ( `' f o. f ) = ( _I |` ( ( 0 ..^ N ) \ dom u ) ) )
226 77 225 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 ) ) )
227 196 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 ) ) )
228 224 226 227 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 ) ) )
229 f1of 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) -1-1-onto-> ( D \ ran u ) -> f : ( ( 0 ..^ N ) \ dom u ) --> ( D \ ran u ) )
230 frn 
 |-  ( f : ( ( 0 ..^ N ) \ dom u ) --> ( D \ ran u ) -> ran f C_ ( D \ ran u ) )
231 cores 
 |-  ( ran f C_ ( D \ ran u ) -> ( ( ( `' ( u u. f ) o. Q ) |` ( D \ ran u ) ) o. f ) = ( ( `' ( u u. f ) o. Q ) o. f ) )
232 77 229 230 231 4syl 
 |-  ( ( ( ( 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 ) )
233 220 228 232 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 ) ) )
234 202 233 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 ) ) )
235 189 234 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 ) ) ) )
236 115 235 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 ) ) ) )
237 vex 
 |-  u e. _V
238 vex 
 |-  f e. _V
239 237 238 unex 
 |-  ( u u. f ) e. _V
240 f1oeq1 
 |-  ( q = ( u u. f ) -> ( q : ( 0 ..^ N ) -1-1-onto-> D <-> ( u u. f ) : ( 0 ..^ N ) -1-1-onto-> D ) )
241 cnveq 
 |-  ( q = ( u u. f ) -> `' q = `' ( u u. f ) )
242 241 coeq1d 
 |-  ( q = ( u u. f ) -> ( `' q o. Q ) = ( `' ( u u. f ) o. Q ) )
243 id 
 |-  ( q = ( u u. f ) -> q = ( u u. f ) )
244 242 243 coeq12d 
 |-  ( q = ( u u. f ) -> ( ( `' q o. Q ) o. q ) = ( ( `' ( u u. f ) o. Q ) o. ( u u. f ) ) )
245 244 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 ) ) ) ) )
246 240 245 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 ) ) ) ) ) )
247 239 246 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 ) ) ) ) )
248 92 236 247 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 ) ) ) ) )
249 73 248 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 ) ) ) ) )
250 nfcv 
 |-  F/_ u M
251 4 2 5 tocycf 
 |-  ( D e. Fin -> M : { w e. Word D | w : dom w -1-1-> D } --> B )
252 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 } )
253 9 251 252 3syl 
 |-  ( ph -> M Fn { w e. Word D | w : dom w -1-1-> D } )
254 10 1 eleqtrdi 
 |-  ( ph -> Q e. ( M " ( `' # " { P } ) ) )
255 250 253 254 fvelimad 
 |-  ( ph -> E. u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ( M ` u ) = Q )
256 249 255 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 ) ) ) ) )