Metamath Proof Explorer

Theorem cshwidxmodr

Description: The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 17-Mar-2021)

Ref Expression
Assertion cshwidxmodr ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) )
2 nn0z ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℤ )
3 2 3ad2ant1 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℤ )
4 zsubcl ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐼 − 𝑁 ) ∈ ℤ )
5 3 4 sylan ⊢ ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝐼 − 𝑁 ) ∈ ℤ )
6 simpl2 ⊢ ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
7 5 6 jca ⊢ ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐼 − 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
8 7 ex ⊢ ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ∈ ℤ → ( ( 𝐼 − 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
9 1 8 sylbi ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ∈ ℤ → ( ( 𝐼 − 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
10 9 impcom ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐼 − 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
11 10 3adant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐼 − 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
12 zmodfzo ⊢ ( ( ( 𝐼 − 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
13 11 12 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
15 13 14 syld3an3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
16 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℤ )
17 16 adantl ⊢ ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ∈ ℤ )
18 17 4 sylan ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝐼 − 𝑁 ) ∈ ℤ )
19 18 zred ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝐼 − 𝑁 ) ∈ ℝ )
20 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
21 20 adantl ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
22 nnrp ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
23 22 ad3antlr ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
24 modaddmod ⊢ ( ( ( 𝐼 − 𝑁 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) → ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝐼 − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
25 19 21 23 24 syl3anc ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝐼 − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
26 nn0cn ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℂ )
27 26 ad2antrr ⊢ ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ∈ ℂ )
28 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
29 npcan ⊢ ( ( 𝐼 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐼 − 𝑁 ) + 𝑁 ) = 𝐼 )
30 27 28 29 syl2an ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐼 − 𝑁 ) + 𝑁 ) = 𝐼 )
31 30 oveq1d ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐼 − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝐼 mod ( ♯ ‘ 𝑊 ) ) )
32 zmodidfzoimp ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 mod ( ♯ ‘ 𝑊 ) ) = 𝐼 )
33 32 ad2antlr ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝐼 mod ( ♯ ‘ 𝑊 ) ) = 𝐼 )
34 25 31 33 3eqtrd ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = 𝐼 )
35 34 fveq2d ⊢ ( ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) )
36 35 ex ⊢ ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑁 ∈ ℤ → ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) ) )
37 36 ex ⊢ ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ∈ ℤ → ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) ) ) )
38 37 3adant3 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ∈ ℤ → ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) ) ) )
39 1 38 sylbi ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ∈ ℤ → ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) ) ) )
40 39 pm2.43i ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ∈ ℤ → ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) ) )
41 40 impcom ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) )
42 41 3adant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) )
43 15 42 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( 𝐼 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝐼 ) )