Metamath Proof Explorer

Theorem tocycfvres2

Description: A cyclic permutation is the identity outside of its orbit. (Contributed by Thierry Arnoux, 15-Oct-2023)

Ref Expression
Hypotheses tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
Assertion tocycfvres2 ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ↾ ( 𝐷 ∖ ran 𝑊 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
4 tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
5 1 2 3 4 tocycfv ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
6 5 reseq1d ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ↾ ( 𝐷 ∖ ran 𝑊 ) ) = ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ↾ ( 𝐷 ∖ ran 𝑊 ) ) )
7 fnresi ⊢ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) Fn ( 𝐷 ∖ ran 𝑊 )
8 7 a1i ⊢ ( 𝜑 → ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) Fn ( 𝐷 ∖ ran 𝑊 ) )
9 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
10 cshwfn ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ) → ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11 3 9 10 syl2anc ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
12 f1f1orn ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
13 f1ocnv ⊢ ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
14 f1ofn ⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 Fn ran 𝑊 )
15 4 12 13 14 4syl ⊢ ( 𝜑 → ◡ 𝑊 Fn ran 𝑊 )
16 dfdm4 ⊢ dom 𝑊 = ran ◡ 𝑊
17 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
18 3 17 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
19 ssidd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
20 18 19 eqsstrd ⊢ ( 𝜑 → dom 𝑊 ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
21 16 20 eqsstrrid ⊢ ( 𝜑 → ran ◡ 𝑊 ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
22 fnco ⊢ ( ( ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ◡ 𝑊 Fn ran 𝑊 ∧ ran ◡ 𝑊 ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) Fn ran 𝑊 )
23 11 15 21 22 syl3anc ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) Fn ran 𝑊 )
24 disjdifr ⊢ ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅
25 24 a1i ⊢ ( 𝜑 → ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅ )
26 fnunres1 ⊢ ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) Fn ( 𝐷 ∖ ran 𝑊 ) ∧ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) Fn ran 𝑊 ∧ ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅ ) → ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ↾ ( 𝐷 ∖ ran 𝑊 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) )
27 8 23 25 26 syl3anc ⊢ ( 𝜑 → ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ↾ ( 𝐷 ∖ ran 𝑊 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) )
28 6 27 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) ↾ ( 𝐷 ∖ ran 𝑊 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) )