Metamath Proof Explorer


Theorem cycpmconjslem2

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

Ref Expression
Hypotheses cycpmconjs.c 𝐶 = ( 𝑀 “ ( ♯ “ { 𝑃 } ) )
cycpmconjs.s 𝑆 = ( SymGrp ‘ 𝐷 )
cycpmconjs.n 𝑁 = ( ♯ ‘ 𝐷 )
cycpmconjs.m 𝑀 = ( toCyc ‘ 𝐷 )
cycpmconjs.b 𝐵 = ( Base ‘ 𝑆 )
cycpmconjs.a + = ( +g𝑆 )
cycpmconjs.l = ( -g𝑆 )
cycpmconjs.p ( 𝜑𝑃 ∈ ( 0 ... 𝑁 ) )
cycpmconjs.d ( 𝜑𝐷 ∈ Fin )
cycpmconjs.q ( 𝜑𝑄𝐶 )
Assertion cycpmconjslem2 ( 𝜑 → ∃ 𝑞 ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto𝐷 ∧ ( ( 𝑞𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )

Proof

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