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 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
cycpmfv1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
Assertion cycpmfv1 ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
4 tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
5 cycpmfv1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
6 lencl ⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
7 3 6 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
8 7 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
9 fzossrbm1 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10 8 9 syl ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11 10 5 sseldd ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
12 1 2 3 4 11 cycpmfvlem ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) )
13 df-f1 ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ↔ ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) )
14 4 13 sylib ⊢ ( 𝜑 → ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) )
15 14 simprd ⊢ ( 𝜑 → Fun ◡ 𝑊 )
16 wrdfn ⊢ ( 𝑊 ∈ Word 𝐷 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
17 3 16 syl ⊢ ( 𝜑 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
18 fnfvelrn ⊢ ( ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑁 ) ∈ ran 𝑊 )
19 17 11 18 syl2anc ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑁 ) ∈ ran 𝑊 )
20 df-rn ⊢ ran 𝑊 = dom ◡ 𝑊
21 19 20 eleqtrdi ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑁 ) ∈ dom ◡ 𝑊 )
22 fvco ⊢ ( ( Fun ◡ 𝑊 ∧ ( 𝑊 ‘ 𝑁 ) ∈ dom ◡ 𝑊 ) → ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( ( 𝑊 cyclShift 1 ) ‘ ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) ) )
23 15 21 22 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( ( 𝑊 cyclShift 1 ) ‘ ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) ) )
24 f1f1orn ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
25 4 24 syl ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
26 17 fndmd ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
27 11 26 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ dom 𝑊 )
28 f1ocnvfv1 ⊢ ( ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 ∧ 𝑁 ∈ dom 𝑊 ) → ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) = 𝑁 )
29 25 27 28 syl2anc ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) = 𝑁 )
30 29 fveq2d ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ‘ ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) ) = ( ( 𝑊 cyclShift 1 ) ‘ 𝑁 ) )
31 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
32 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 1 ) ‘ 𝑁 ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) ) )
33 3 31 11 32 syl3anc ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ‘ 𝑁 ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) ) )
34 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) )
35 fzoaddel2 ⊢ ( ( 𝑁 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑁 + 1 ) ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) )
36 5 8 31 35 syl3anc ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) )
37 34 36 sselid ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 zmodidfzoimp ⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑁 + 1 ) )
39 37 38 syl ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑁 + 1 ) )
40 39 fveq2d ⊢ ( 𝜑 → ( 𝑊 ‘ ( ( 𝑁 + 1 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
41 30 33 40 3eqtrd ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ‘ ( ◡ 𝑊 ‘ ( 𝑊 ‘ 𝑁 ) ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
42 12 23 41 3eqtrd ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ‘ ( 𝑊 ‘ 𝑁 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )