Metamath Proof Explorer

Theorem cycpmrn

Description: The range of the word used to build a cycle is the cycle's orbit, i.e., the set of points it moves. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Hypotheses cycpmrn.1 ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
cycpmrn.2 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
cycpmrn.3 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
cycpmrn.4 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
cycpmrn.5 ⊢ ( 𝜑 → 1 < ( ♯ ‘ 𝑊 ) )
Assertion cycpmrn ( 𝜑 → ran 𝑊 = dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) )

Proof

Step Hyp Ref Expression
1 cycpmrn.1 ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
2 cycpmrn.2 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 cycpmrn.3 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
4 cycpmrn.4 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
5 cycpmrn.5 ⊢ ( 𝜑 → 1 < ( ♯ ‘ 𝑊 ) )
6 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
7 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑥 ∈ dom 𝑊 )
8 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) )
9 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
10 lencl ⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
11 3 10 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
12 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
13 12 nn0zd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
14 1zzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 1 ∈ ℤ )
15 fzoaddel2 ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑥 + 1 ) ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) )
16 9 13 14 15 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑥 + 1 ) ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) )
17 8 16 sselid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑥 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
18 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑊 ∈ Word 𝐷 )
19 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
20 18 19 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
21 17 20 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑥 + 1 ) ∈ dom 𝑊 )
22 fzossz ⊢ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⊆ ℤ
23 22 9 sselid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑥 ∈ ℤ )
24 23 zred ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑥 ∈ ℝ )
25 24 ltp1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑥 < ( 𝑥 + 1 ) )
26 24 25 ltned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑥 ≠ ( 𝑥 + 1 ) )
27 f1veqaeq ⊢ ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ ( 𝑥 ∈ dom 𝑊 ∧ ( 𝑥 + 1 ) ∈ dom 𝑊 ) ) → ( ( 𝑊 ‘ 𝑥 ) = ( 𝑊 ‘ ( 𝑥 + 1 ) ) → 𝑥 = ( 𝑥 + 1 ) ) )
28 27 necon3d ⊢ ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ ( 𝑥 ∈ dom 𝑊 ∧ ( 𝑥 + 1 ) ∈ dom 𝑊 ) ) → ( 𝑥 ≠ ( 𝑥 + 1 ) → ( 𝑊 ‘ 𝑥 ) ≠ ( 𝑊 ‘ ( 𝑥 + 1 ) ) ) )
29 28 anassrs ⊢ ( ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑥 ∈ dom 𝑊 ) ∧ ( 𝑥 + 1 ) ∈ dom 𝑊 ) → ( 𝑥 ≠ ( 𝑥 + 1 ) → ( 𝑊 ‘ 𝑥 ) ≠ ( 𝑊 ‘ ( 𝑥 + 1 ) ) ) )
30 29 imp ⊢ ( ( ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑥 ∈ dom 𝑊 ) ∧ ( 𝑥 + 1 ) ∈ dom 𝑊 ) ∧ 𝑥 ≠ ( 𝑥 + 1 ) ) → ( 𝑊 ‘ 𝑥 ) ≠ ( 𝑊 ‘ ( 𝑥 + 1 ) ) )
31 6 7 21 26 30 syl1111anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑊 ‘ 𝑥 ) ≠ ( 𝑊 ‘ ( 𝑥 + 1 ) ) )
32 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝐷 ∈ 𝑉 )
33 1 32 18 6 9 cycpmfv1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑥 ) ) = ( 𝑊 ‘ ( 𝑥 + 1 ) ) )
34 31 33 neeqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑊 ‘ 𝑥 ) ≠ ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑥 ) ) )
35 34 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑥 ) ) ≠ ( 𝑊 ‘ 𝑥 ) )
36 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑦 = ( 𝑊 ‘ 𝑥 ) )
37 36 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑥 ) ) )
38 35 37 36 3netr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) ≠ 𝑦 )
39 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
40 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → 𝑊 ∈ Word 𝐷 )
41 eldmne0 ⊢ ( 𝑥 ∈ dom 𝑊 → 𝑊 ≠ ∅ )
42 41 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → 𝑊 ≠ ∅ )
43 lennncl ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
44 40 42 43 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
45 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
46 44 45 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
47 40 19 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
48 46 47 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → 0 ∈ dom 𝑊 )
49 48 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 0 ∈ dom 𝑊 )
50 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 𝑥 ∈ dom 𝑊 )
51 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
52 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
53 11 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
54 52 53 posdifd ⊢ ( 𝜑 → ( 1 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
55 5 54 mpbid ⊢ ( 𝜑 → 0 < ( ( ♯ ‘ 𝑊 ) − 1 ) )
56 51 55 ltned ⊢ ( 𝜑 → 0 ≠ ( ( ♯ ‘ 𝑊 ) − 1 ) )
57 56 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 0 ≠ ( ( ♯ ‘ 𝑊 ) − 1 ) )
58 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) )
59 57 58 neeqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 0 ≠ 𝑥 )
60 f1veqaeq ⊢ ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ ( 0 ∈ dom 𝑊 ∧ 𝑥 ∈ dom 𝑊 ) ) → ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 𝑥 ) → 0 = 𝑥 ) )
61 60 necon3d ⊢ ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ ( 0 ∈ dom 𝑊 ∧ 𝑥 ∈ dom 𝑊 ) ) → ( 0 ≠ 𝑥 → ( 𝑊 ‘ 0 ) ≠ ( 𝑊 ‘ 𝑥 ) ) )
62 61 anassrs ⊢ ( ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 0 ∈ dom 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) → ( 0 ≠ 𝑥 → ( 𝑊 ‘ 0 ) ≠ ( 𝑊 ‘ 𝑥 ) ) )
63 62 imp ⊢ ( ( ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 0 ∈ dom 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 0 ≠ 𝑥 ) → ( 𝑊 ‘ 0 ) ≠ ( 𝑊 ‘ 𝑥 ) )
64 39 49 50 59 63 syl1111anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( 𝑊 ‘ 0 ) ≠ ( 𝑊 ‘ 𝑥 ) )
65 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 𝑦 = ( 𝑊 ‘ 𝑥 ) )
66 65 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑥 ) ) )
67 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 𝐷 ∈ 𝑉 )
68 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 𝑊 ∈ Word 𝐷 )
69 44 nngt0d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
70 69 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
71 1 67 68 39 70 58 cycpmfv2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑥 ) ) = ( 𝑊 ‘ 0 ) )
72 66 71 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑊 ‘ 0 ) )
73 64 72 65 3netr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) ≠ 𝑦 )
74 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → 𝑥 ∈ dom 𝑊 )
75 74 47 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
76 0z ⊢ 0 ∈ ℤ
77 0p1e1 ⊢ ( 0 + 1 ) = 1
78 77 fveq2i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
79 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
80 78 79 eqtr4i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ℕ
81 44 80 eleqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
82 fzosplitsnm1 ⊢ ( ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
83 76 81 82 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
84 75 83 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → 𝑥 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
85 elun ⊢ ( 𝑥 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∨ 𝑥 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
86 84 85 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∨ 𝑥 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
87 velsn ⊢ ( 𝑥 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ↔ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) )
88 87 orbi2i ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∨ 𝑥 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∨ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
89 86 88 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∨ 𝑥 = ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
90 38 73 89 mpjaodan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) ∧ 𝑥 ∈ dom 𝑊 ) ∧ 𝑦 = ( 𝑊 ‘ 𝑥 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) ≠ 𝑦 )
91 f1fun ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → Fun 𝑊 )
92 elrnrexdmb ⊢ ( Fun 𝑊 → ( 𝑦 ∈ ran 𝑊 ↔ ∃ 𝑥 ∈ dom 𝑊 𝑦 = ( 𝑊 ‘ 𝑥 ) ) )
93 4 91 92 3syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝑊 ↔ ∃ 𝑥 ∈ dom 𝑊 𝑦 = ( 𝑊 ‘ 𝑥 ) ) )
94 93 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) → ∃ 𝑥 ∈ dom 𝑊 𝑦 = ( 𝑊 ‘ 𝑥 ) )
95 90 94 r19.29a ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) ≠ 𝑦 )
96 eqid ⊢ ( SymGrp ‘ 𝐷 ) = ( SymGrp ‘ 𝐷 )
97 1 2 3 4 96 cycpmcl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑊 ) ∈ ( Base ‘ ( SymGrp ‘ 𝐷 ) ) )
98 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝐷 ) ) = ( Base ‘ ( SymGrp ‘ 𝐷 ) )
99 96 98 elsymgbas ⊢ ( 𝐷 ∈ 𝑉 → ( ( 𝑀 ‘ 𝑊 ) ∈ ( Base ‘ ( SymGrp ‘ 𝐷 ) ) ↔ ( 𝑀 ‘ 𝑊 ) : 𝐷 –1-1-onto→ 𝐷 ) )
100 2 99 syl ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ∈ ( Base ‘ ( SymGrp ‘ 𝐷 ) ) ↔ ( 𝑀 ‘ 𝑊 ) : 𝐷 –1-1-onto→ 𝐷 ) )
101 97 100 mpbid ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑊 ) : 𝐷 –1-1-onto→ 𝐷 )
102 f1ofn ⊢ ( ( 𝑀 ‘ 𝑊 ) : 𝐷 –1-1-onto→ 𝐷 → ( 𝑀 ‘ 𝑊 ) Fn 𝐷 )
103 101 102 syl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑊 ) Fn 𝐷 )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) → ( 𝑀 ‘ 𝑊 ) Fn 𝐷 )
105 wrdf ⊢ ( 𝑊 ∈ Word 𝐷 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 )
106 frn ⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 → ran 𝑊 ⊆ 𝐷 )
107 3 105 106 3syl ⊢ ( 𝜑 → ran 𝑊 ⊆ 𝐷 )
108 107 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) → 𝑦 ∈ 𝐷 )
109 fnelnfp ⊢ ( ( ( 𝑀 ‘ 𝑊 ) Fn 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑦 ∈ dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) ↔ ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) ≠ 𝑦 ) )
110 104 108 109 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) → ( 𝑦 ∈ dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) ↔ ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑦 ) ≠ 𝑦 ) )
111 95 110 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑊 ) → 𝑦 ∈ dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) )
112 111 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝑊 → 𝑦 ∈ dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) ) )
113 112 ssrdv ⊢ ( 𝜑 → ran 𝑊 ⊆ dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) )
114 1 2 3 4 tocycfv ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
115 114 difeq1d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ∖ I ) = ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∖ I ) )
116 115 dmeqd ⊢ ( 𝜑 → dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) = dom ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∖ I ) )
117 difundir ⊢ ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∖ I ) = ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∖ I ) ∪ ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) )
118 resdifcom ⊢ ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∖ I ) = ( ( I ∖ I ) ↾ ( 𝐷 ∖ ran 𝑊 ) )
119 difid ⊢ ( I ∖ I ) = ∅
120 119 reseq1i ⊢ ( ( I ∖ I ) ↾ ( 𝐷 ∖ ran 𝑊 ) ) = ( ∅ ↾ ( 𝐷 ∖ ran 𝑊 ) )
121 0res ⊢ ( ∅ ↾ ( 𝐷 ∖ ran 𝑊 ) ) = ∅
122 118 120 121 3eqtri ⊢ ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∖ I ) = ∅
123 122 uneq1i ⊢ ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∖ I ) ∪ ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) ) = ( ∅ ∪ ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) )
124 0un ⊢ ( ∅ ∪ ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) ) = ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I )
125 117 123 124 3eqtri ⊢ ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∖ I ) = ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I )
126 125 dmeqi ⊢ dom ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∖ I ) = dom ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I )
127 difss ⊢ ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) ⊆ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 )
128 dmss ⊢ ( ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) ⊆ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) → dom ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) ⊆ dom ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) )
129 127 128 ax-mp ⊢ dom ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) ⊆ dom ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 )
130 dmcoss ⊢ dom ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ⊆ dom ◡ 𝑊
131 df-rn ⊢ ran 𝑊 = dom ◡ 𝑊
132 130 131 sseqtrri ⊢ dom ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ⊆ ran 𝑊
133 129 132 sstri ⊢ dom ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∖ I ) ⊆ ran 𝑊
134 126 133 eqsstri ⊢ dom ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∖ I ) ⊆ ran 𝑊
135 116 134 eqsstrdi ⊢ ( 𝜑 → dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) ⊆ ran 𝑊 )
136 113 135 eqssd ⊢ ( 𝜑 → ran 𝑊 = dom ( ( 𝑀 ‘ 𝑊 ) ∖ I ) )