Metamath Proof Explorer

Theorem 1cshid

Description: Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023)

Ref Expression
Assertion 1cshid ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 cyclShift 𝑁 ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 cshwmodn ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
2 1 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
3 simp3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ♯ ‘ 𝑊 ) = 1 )
4 3 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = ( 𝑁 mod 1 ) )
5 zmod10 ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 mod 1 ) = 0 )
6 5 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑁 mod 1 ) = 0 )
7 4 6 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = 0 )
8 7 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 cyclShift 0 ) )
9 cshw0 ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = 𝑊 )
10 9 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 cyclShift 0 ) = 𝑊 )
11 2 8 10 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 cyclShift 𝑁 ) = 𝑊 )