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