Metamath Proof Explorer

Theorem cshwidx0

Description: The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N of the original word. (Contributed by AV, 15-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion cshwidx0 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 hasheq0 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = 0 ↔ 𝑊 = ∅ ) )
2 elfzo0 ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) )
3 elnnne0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) )
4 eqneqall ⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
5 4 com12 ⊢ ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
6 5 adantl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
7 3 6 sylbi ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
8 7 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
9 2 8 sylbi ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
10 9 com13 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
11 1 10 sylbird ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ∅ → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
12 11 com23 ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 = ∅ → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
13 12 imp ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 = ∅ → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) )
14 13 com12 ⊢ ( 𝑊 = ∅ → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) )
15 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
16 15 adantl ⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑊 ∈ Word 𝑉 )
17 simpl ⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑊 ≠ ∅ )
18 elfzoelz ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ )
19 18 ad2antll ⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑁 ∈ ℤ )
20 cshwidx0mod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
21 16 17 19 20 syl3anc ⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
22 zmodidfzoimp ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = 𝑁 )
23 22 ad2antll ⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = 𝑁 )
24 23 fveq2d ⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝑁 ) )
25 21 24 eqtrd ⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) )
26 25 ex ⊢ ( 𝑊 ≠ ∅ → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) )
27 14 26 pm2.61ine ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) )