Metamath Proof Explorer

Theorem tocycfvres1

Description: A cyclic permutation is a cyclic shift on its orbit. (Contributed by Thierry Arnoux, 15-Oct-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
Assertion tocycfvres1 ⊢ φ → C ⁡ W ↾ ran ⁡ W = W cyclShift 1 ∘ W -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 1 2 3 4 tocycfv ⊢ φ → C ⁡ W = I ↾ D ∖ ran ⁡ W ∪ W cyclShift 1 ∘ W -1
6 5 reseq1d ⊢ φ → C ⁡ W ↾ ran ⁡ W = I ↾ D ∖ ran ⁡ W ∪ W cyclShift 1 ∘ W -1 ↾ ran ⁡ W
7 fnresi ⊢ I ↾ D ∖ ran ⁡ W Fn D ∖ ran ⁡ W
8 7 a1i ⊢ φ → I ↾ D ∖ ran ⁡ W Fn D ∖ ran ⁡ W
9 1zzd ⊢ φ → 1 ∈ ℤ
10 cshwfn ⊢ W ∈ Word D ∧ 1 ∈ ℤ → W cyclShift 1 Fn 0 ..^ W
11 3 9 10 syl2anc ⊢ φ → W cyclShift 1 Fn 0 ..^ W
12 f1f1orn ⊢ W : dom ⁡ W ⟶ 1-1 D → W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W
13 f1ocnv ⊢ W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W → W -1 : ran ⁡ W ⟶ 1-1 onto dom ⁡ W
14 f1ofn ⊢ W -1 : ran ⁡ W ⟶ 1-1 onto dom ⁡ W → W -1 Fn ran ⁡ W
15 4 12 13 14 4syl ⊢ φ → W -1 Fn ran ⁡ W
16 dfdm4 ⊢ dom ⁡ W = ran ⁡ W -1
17 wrddm ⊢ W ∈ Word D → dom ⁡ W = 0 ..^ W
18 3 17 syl ⊢ φ → dom ⁡ W = 0 ..^ W
19 ssidd ⊢ φ → 0 ..^ W ⊆ 0 ..^ W
20 18 19 eqsstrd ⊢ φ → dom ⁡ W ⊆ 0 ..^ W
21 16 20 eqsstrrid ⊢ φ → ran ⁡ W -1 ⊆ 0 ..^ W
22 fnco ⊢ W cyclShift 1 Fn 0 ..^ W ∧ W -1 Fn ran ⁡ W ∧ ran ⁡ W -1 ⊆ 0 ..^ W → W cyclShift 1 ∘ W -1 Fn ran ⁡ W
23 11 15 21 22 syl3anc ⊢ φ → W cyclShift 1 ∘ W -1 Fn ran ⁡ W
24 disjdifr ⊢ D ∖ ran ⁡ W ∩ ran ⁡ W = ∅
25 24 a1i ⊢ φ → D ∖ ran ⁡ W ∩ ran ⁡ W = ∅
26 fnunres2 ⊢ I ↾ D ∖ ran ⁡ W Fn D ∖ ran ⁡ W ∧ W cyclShift 1 ∘ W -1 Fn ran ⁡ W ∧ D ∖ ran ⁡ W ∩ ran ⁡ W = ∅ → I ↾ D ∖ ran ⁡ W ∪ W cyclShift 1 ∘ W -1 ↾ ran ⁡ W = W cyclShift 1 ∘ W -1
27 8 23 25 26 syl3anc ⊢ φ → I ↾ D ∖ ran ⁡ W ∪ W cyclShift 1 ∘ W -1 ↾ ran ⁡ W = W cyclShift 1 ∘ W -1
28 6 27 eqtrd ⊢ φ → C ⁡ W ↾ ran ⁡ W = W cyclShift 1 ∘ W -1