Metamath Proof Explorer

Theorem tocycfv

Description: Function value of a permutation cycle built from a word. (Contributed by Thierry Arnoux, 18-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
Assertion tocycfv ⊢ φ → C ⁡ W = I ↾ D ∖ 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 tocycval ⊢ D ∈ V → C = w ∈ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D ⟼ I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1
6 2 5 syl ⊢ φ → C = w ∈ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D ⟼ I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1
7 simpr ⊢ φ ∧ w = W → w = W
8 7 rneqd ⊢ φ ∧ w = W → ran ⁡ w = ran ⁡ W
9 8 difeq2d ⊢ φ ∧ w = W → D ∖ ran ⁡ w = D ∖ ran ⁡ W
10 9 reseq2d ⊢ φ ∧ w = W → I ↾ D ∖ ran ⁡ w = I ↾ D ∖ ran ⁡ W
11 7 oveq1d ⊢ φ ∧ w = W → w cyclShift 1 = W cyclShift 1
12 7 cnveqd ⊢ φ ∧ w = W → w -1 = W -1
13 11 12 coeq12d ⊢ φ ∧ w = W → w cyclShift 1 ∘ w -1 = W cyclShift 1 ∘ W -1
14 10 13 uneq12d ⊢ φ ∧ w = W → I ↾ D ∖ ran ⁡ w ∪ w cyclShift 1 ∘ w -1 = I ↾ D ∖ ran ⁡ W ∪ W cyclShift 1 ∘ W -1
15 id ⊢ u = W → u = W
16 dmeq ⊢ u = W → dom ⁡ u = dom ⁡ W
17 eqidd ⊢ u = W → D = D
18 15 16 17 f1eq123d ⊢ u = W → u : dom ⁡ u ⟶ 1-1 D ↔ W : dom ⁡ W ⟶ 1-1 D
19 18 3 4 elrabd ⊢ φ → W ∈ u ∈ Word D | u : dom ⁡ u ⟶ 1-1 D
20 2 difexd ⊢ φ → D ∖ ran ⁡ W ∈ V
21 20 resiexd ⊢ φ → I ↾ D ∖ ran ⁡ W ∈ V
22 cshwcl ⊢ W ∈ Word D → W cyclShift 1 ∈ Word D
23 3 22 syl ⊢ φ → W cyclShift 1 ∈ Word D
24 cnvexg ⊢ W ∈ Word D → W -1 ∈ V
25 3 24 syl ⊢ φ → W -1 ∈ V
26 coexg ⊢ W cyclShift 1 ∈ Word D ∧ W -1 ∈ V → W cyclShift 1 ∘ W -1 ∈ V
27 23 25 26 syl2anc ⊢ φ → W cyclShift 1 ∘ W -1 ∈ V
28 unexg ⊢ I ↾ D ∖ ran ⁡ W ∈ V ∧ W cyclShift 1 ∘ W -1 ∈ V → I ↾ D ∖ ran ⁡ W ∪ W cyclShift 1 ∘ W -1 ∈ V
29 21 27 28 syl2anc ⊢ φ → I ↾ D ∖ ran ⁡ W ∪ W cyclShift 1 ∘ W -1 ∈ V
30 6 14 19 29 fvmptd ⊢ φ → C ⁡ W = I ↾ D ∖ ran ⁡ W ∪ W cyclShift 1 ∘ W -1