Metamath Proof Explorer

Theorem cycpmfv1

Description: Value of a cycle function for any element but the last. (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
cycpmfv1.1 ⊢ φ → N ∈ 0 ..^ W − 1
Assertion cycpmfv1 ⊢ φ → C ⁡ W ⁡ W ⁡ N = W ⁡ N + 1

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 cycpmfv1.1 ⊢ φ → N ∈ 0 ..^ W − 1
6 lencl ⊢ W ∈ Word D → W ∈ ℕ 0
7 3 6 syl ⊢ φ → W ∈ ℕ 0
8 7 nn0zd ⊢ φ → W ∈ ℤ
9 fzossrbm1 ⊢ W ∈ ℤ → 0 ..^ W − 1 ⊆ 0 ..^ W
10 8 9 syl ⊢ φ → 0 ..^ W − 1 ⊆ 0 ..^ W
11 10 5 sseldd ⊢ φ → N ∈ 0 ..^ W
12 1 2 3 4 11 cycpmfvlem ⊢ φ → C ⁡ W ⁡ W ⁡ N = W cyclShift 1 ∘ W -1 ⁡ W ⁡ N
13 df-f1 ⊢ W : dom ⁡ W ⟶ 1-1 D ↔ W : dom ⁡ W ⟶ D ∧ Fun ⁡ W -1
14 4 13 sylib ⊢ φ → W : dom ⁡ W ⟶ D ∧ Fun ⁡ W -1
15 14 simprd ⊢ φ → Fun ⁡ W -1
16 wrdfn ⊢ W ∈ Word D → W Fn 0 ..^ W
17 3 16 syl ⊢ φ → W Fn 0 ..^ W
18 fnfvelrn ⊢ W Fn 0 ..^ W ∧ N ∈ 0 ..^ W → W ⁡ N ∈ ran ⁡ W
19 17 11 18 syl2anc ⊢ φ → W ⁡ N ∈ ran ⁡ W
20 df-rn ⊢ ran ⁡ W = dom ⁡ W -1
21 19 20 eleqtrdi ⊢ φ → W ⁡ N ∈ dom ⁡ W -1
22 fvco ⊢ Fun ⁡ W -1 ∧ W ⁡ N ∈ dom ⁡ W -1 → W cyclShift 1 ∘ W -1 ⁡ W ⁡ N = W cyclShift 1 ⁡ W -1 ⁡ W ⁡ N
23 15 21 22 syl2anc ⊢ φ → W cyclShift 1 ∘ W -1 ⁡ W ⁡ N = W cyclShift 1 ⁡ W -1 ⁡ W ⁡ N
24 f1f1orn ⊢ W : dom ⁡ W ⟶ 1-1 D → W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W
25 4 24 syl ⊢ φ → W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W
26 17 fndmd ⊢ φ → dom ⁡ W = 0 ..^ W
27 11 26 eleqtrrd ⊢ φ → N ∈ dom ⁡ W
28 f1ocnvfv1 ⊢ W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W ∧ N ∈ dom ⁡ W → W -1 ⁡ W ⁡ N = N
29 25 27 28 syl2anc ⊢ φ → W -1 ⁡ W ⁡ N = N
30 29 fveq2d ⊢ φ → W cyclShift 1 ⁡ W -1 ⁡ W ⁡ N = W cyclShift 1 ⁡ N
31 1zzd ⊢ φ → 1 ∈ ℤ
32 cshwidxmod ⊢ W ∈ Word D ∧ 1 ∈ ℤ ∧ N ∈ 0 ..^ W → W cyclShift 1 ⁡ N = W ⁡ N + 1 mod W
33 3 31 11 32 syl3anc ⊢ φ → W cyclShift 1 ⁡ N = W ⁡ N + 1 mod W
34 fzo0ss1 ⊢ 1 ..^ W ⊆ 0 ..^ W
35 fzoaddel2 ⊢ N ∈ 0 ..^ W − 1 ∧ W ∈ ℤ ∧ 1 ∈ ℤ → N + 1 ∈ 1 ..^ W
36 5 8 31 35 syl3anc ⊢ φ → N + 1 ∈ 1 ..^ W
37 34 36 sseldi ⊢ φ → N + 1 ∈ 0 ..^ W
38 zmodidfzoimp ⊢ N + 1 ∈ 0 ..^ W → N + 1 mod W = N + 1
39 37 38 syl ⊢ φ → N + 1 mod W = N + 1
40 39 fveq2d ⊢ φ → W ⁡ N + 1 mod W = W ⁡ N + 1
41 30 33 40 3eqtrd ⊢ φ → W cyclShift 1 ⁡ W -1 ⁡ W ⁡ N = W ⁡ N + 1
42 12 23 41 3eqtrd ⊢ φ → C ⁡ W ⁡ W ⁡ N = W ⁡ N + 1