Metamath Proof Explorer

Theorem cycpmfv2

Description: Value of a cycle function for the last element of the orbit. (Contributed by Thierry Arnoux, 22-Sep-2023)

Ref Expression
Hypotheses tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
cycpmfv2.1 ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑊 ) )
cycpmfv2.2 ⊢ ( 𝜑 → 𝑁 = ( ( ♯ ‘ 𝑊 ) − 1 ) )
Assertion cycpmfv2 ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( 𝑊 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
4 tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
5 cycpmfv2.1 ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑊 ) )
6 cycpmfv2.2 ⊢ ( 𝜑 → 𝑁 = ( ( ♯ ‘ 𝑊 ) − 1 ) )
7 lencl ⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
8 3 7 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
9 elnnnn0b ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝑊 ) ) )
10 8 5 9 sylanbrc ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ )
11 elfz1end ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
12 10 11 sylib ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
13 fz1fzo0m1 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14 12 13 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
15 6 14 eqeltrd ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
16 1 2 3 4 15 cycpmfvlem ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) )
17 df-f1 ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ↔ ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) )
18 4 17 sylib ⊢ ( 𝜑 → ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) )
19 18 simprd ⊢ ( 𝜑 → Fun ◡ 𝑊 )
20 wrdfn ⊢ ( 𝑊 ∈ Word 𝐷 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
21 3 20 syl ⊢ ( 𝜑 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
22 fnfvelrn ⊢ ( ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑁 ) ∈ ran 𝑊 )
23 21 15 22 syl2anc ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑁 ) ∈ ran 𝑊 )
24 df-rn ⊢ ran 𝑊 = dom ◡ 𝑊
25 23 24 eleqtrdi ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑁 ) ∈ dom ◡ 𝑊 )
26 fvco ⊢ ( ( Fun ◡ 𝑊 ∧ ( 𝑊 ‘ 𝑁 ) ∈ dom ◡ 𝑊 ) → ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( ( 𝑊 cyclShift 1 ) ‘ ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) ) )
27 19 25 26 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( ( 𝑊 cyclShift 1 ) ‘ ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) ) )
28 f1f1orn ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
29 4 28 syl ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
30 21 fndmd ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
31 15 30 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ dom 𝑊 )
32 f1ocnvfv1 ⊢ ( ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 ∧ 𝑁 ∈ dom 𝑊 ) → ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) = 𝑁 )
33 29 31 32 syl2anc ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) = 𝑁 )
34 33 fveq2d ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ‘ ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) ) = ( ( 𝑊 cyclShift 1 ) ‘ 𝑁 ) )
35 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
36 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 1 ) ‘ 𝑁 ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) ) )
37 3 35 15 36 syl3anc ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ‘ 𝑁 ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) ) )
38 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) )
39 fzssz ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℤ
40 38 39 sstri ⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ℤ
41 40 15 sselid ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
42 41 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
43 10 nnrpd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
44 6 oveq1d ⊢ ( 𝜑 → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) mod ( ♯ ‘ 𝑊 ) ) )
45 zmodidfzoimp ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
46 14 45 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
47 44 46 eqtrd ⊢ ( 𝜑 → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
48 modm1p1mod0 ⊢ ( ( 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) → ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) )
49 48 imp ⊢ ( ( ( 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) ∧ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
50 42 43 47 49 syl21anc ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
51 50 fveq2d ⊢ ( 𝜑 → ( 𝑊 ‘ ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 0 ) )
52 34 37 51 3eqtrd ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ‘ ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) ) = ( 𝑊 ‘ 0 ) )
53 16 27 52 3eqtrd ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( 𝑊 ‘ 0 ) )