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 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
Assertion tocycfv ( 𝜑 → ( 𝐶 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
4 tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
5 1 tocycval ⊢ ( 𝐷 ∈ 𝑉 → 𝐶 = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )
6 2 5 syl ⊢ ( 𝜑 → 𝐶 = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → 𝑤 = 𝑊 )
8 7 rneqd ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → ran 𝑤 = ran 𝑊 )
9 8 difeq2d ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → ( 𝐷 ∖ ran 𝑤 ) = ( 𝐷 ∖ ran 𝑊 ) )
10 9 reseq2d ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) )
11 7 oveq1d ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → ( 𝑤 cyclShift 1 ) = ( 𝑊 cyclShift 1 ) )
12 7 cnveqd ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → ◡ 𝑤 = ◡ 𝑊 )
13 11 12 coeq12d ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) = ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) )
14 10 13 uneq12d ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
15 id ⊢ ( 𝑢 = 𝑊 → 𝑢 = 𝑊 )
16 dmeq ⊢ ( 𝑢 = 𝑊 → dom 𝑢 = dom 𝑊 )
17 eqidd ⊢ ( 𝑢 = 𝑊 → 𝐷 = 𝐷 )
18 15 16 17 f1eq123d ⊢ ( 𝑢 = 𝑊 → ( 𝑢 : dom 𝑢 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
19 18 3 4 elrabd ⊢ ( 𝜑 → 𝑊 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } )
20 2 difexd ⊢ ( 𝜑 → ( 𝐷 ∖ ran 𝑊 ) ∈ V )
21 20 resiexd ⊢ ( 𝜑 → ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∈ V )
22 cshwcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 cyclShift 1 ) ∈ Word 𝐷 )
23 3 22 syl ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) ∈ Word 𝐷 )
24 cnvexg ⊢ ( 𝑊 ∈ Word 𝐷 → ◡ 𝑊 ∈ V )
25 3 24 syl ⊢ ( 𝜑 → ◡ 𝑊 ∈ V )
26 coexg ⊢ ( ( ( 𝑊 cyclShift 1 ) ∈ Word 𝐷 ∧ ◡ 𝑊 ∈ V ) → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∈ V )
27 23 25 26 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∈ V )
28 unexg ⊢ ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∈ V ∧ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∈ V ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∈ V )
29 21 27 28 syl2anc ⊢ ( 𝜑 → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∈ V )
30 6 14 19 29 fvmptd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )