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∈WordD
tocycfv.1 ⊢φ→W:dom⁡W⟶1-1D
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∈WordD
4 tocycfv.1 ⊢φ→W:dom⁡W⟶1-1D
5 cycpmfv1.1 ⊢φ→N∈0..^W−1
6 lencl ⊢W∈WordD→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=WcyclShift1∘W-1⁡W⁡N
13 df-f1 ⊢W:dom⁡W⟶1-1D↔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∈WordD→WFn0..^W
17 3 16 syl ⊢φ→WFn0..^W
18 fnfvelrn ⊢WFn0..^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→WcyclShift1∘W-1⁡W⁡N=WcyclShift1⁡W-1⁡W⁡N
23 15 21 22 syl2anc ⊢φ→WcyclShift1∘W-1⁡W⁡N=WcyclShift1⁡W-1⁡W⁡N
24 f1f1orn ⊢W:dom⁡W⟶1-1D→W:dom⁡W⟶1-1 ontoran⁡W
25 4 24 syl ⊢φ→W:dom⁡W⟶1-1 ontoran⁡W
26 17 fndmd ⊢φ→dom⁡W=0..^W
27 11 26 eleqtrrd ⊢φ→N∈dom⁡W
28 f1ocnvfv1 ⊢W:dom⁡W⟶1-1 ontoran⁡W∧N∈dom⁡W→W-1⁡W⁡N=N
29 25 27 28 syl2anc ⊢φ→W-1⁡W⁡N=N
30 29 fveq2d ⊢φ→WcyclShift1⁡W-1⁡W⁡N=WcyclShift1⁡N
31 1zzd ⊢φ→1∈ℤ
32 cshwidxmod ⊢W∈WordD∧1∈ℤ∧N∈0..^W→WcyclShift1⁡N=W⁡N+1modW
33 3 31 11 32 syl3anc ⊢φ→WcyclShift1⁡N=W⁡N+1modW
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 sselid ⊢φ→N+1∈0..^W
38 zmodidfzoimp ⊢N+1∈0..^W→N+1modW=N+1
39 37 38 syl ⊢φ→N+1modW=N+1
40 39 fveq2d ⊢φ→W⁡N+1modW=W⁡N+1
41 30 33 40 3eqtrd ⊢φ→WcyclShift1⁡W-1⁡W⁡N=W⁡N+1
42 12 23 41 3eqtrd ⊢φ→C⁡W⁡W⁡N=W⁡N+1