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 ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = 𝑊 )