This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2cshwid

Description: Cyclically shifting a word two times resulting in the word itself. (Contributed by AV, 7-Apr-2018) (Revised by AV, 5-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion 2cshwid ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
2 1 nn0zd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
3 zsubcl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ∈ ℤ )
4 2 3 sylan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ∈ ℤ )
5 2cshw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = ( 𝑊 cyclShift ( 𝑁 + ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) ) )
6 4 5 mpd3an3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = ( 𝑊 cyclShift ( 𝑁 + ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) ) )
7 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
8 1 nn0cnd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
9 pncan3 ⊢ ( ( 𝑁 ∈ ℂ ∧ ( ♯ ‘ 𝑊 ) ∈ ℂ ) → ( 𝑁 + ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
10 7 8 9 syl2anr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑁 + ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
11 10 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift ( 𝑁 + ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) ) = ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) )
12 cshwn ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
13 12 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
14 6 11 13 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = 𝑊 )