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 ⊢ C = toCyc ⁡ D
tocycfv.d ⊢ φ → D ∈ V
tocycfv.w ⊢ φ → W ∈ Word D
tocycfv.1 ⊢ φ → W : dom ⁡ W ⟶ 1-1 D
cycpmfv2.1 ⊢ φ → 0 < W
cycpmfv2.2 ⊢ φ → N = W − 1
Assertion cycpmfv2 ⊢ φ → C ⁡ W ⁡ W ⁡ N = W ⁡ 0

Proof

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