Metamath Proof Explorer

Theorem repswcshw

Description: A cyclically shifted "repeated symbol word". (Contributed by Alexander van der Vekens, 7-Nov-2018) (Proof shortened by AV, 16-Oct-2022)

Ref Expression
Assertion repswcshw ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 𝑁 ) )

Proof

Step Hyp Ref Expression
1 0csh0 ⊢ ( ∅ cyclShift 𝐼 ) = ∅
2 repsw0 ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 0 ) = ∅ )
3 2 oveq1d ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑆 repeatS 0 ) cyclShift 𝐼 ) = ( ∅ cyclShift 𝐼 ) )
4 1 3 2 3eqtr4a ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑆 repeatS 0 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 0 ) )
5 4 3ad2ant1 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 0 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 0 ) )
6 oveq2 ⊢ ( 𝑁 = 0 → ( 𝑆 repeatS 𝑁 ) = ( 𝑆 repeatS 0 ) )
7 6 oveq1d ⊢ ( 𝑁 = 0 → ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( ( 𝑆 repeatS 0 ) cyclShift 𝐼 ) )
8 7 6 eqeq12d ⊢ ( 𝑁 = 0 → ( ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 𝑁 ) ↔ ( ( 𝑆 repeatS 0 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 0 ) ) )
9 5 8 imbitrrid ⊢ ( 𝑁 = 0 → ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 𝑁 ) ) )
10 idd ⊢ ( ¬ 𝑁 = 0 → ( 𝑆 ∈ 𝑉 → 𝑆 ∈ 𝑉 ) )
11 df-ne ⊢ ( 𝑁 ≠ 0 ↔ ¬ 𝑁 = 0 )
12 elnnne0 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
13 12 simplbi2com ⊢ ( 𝑁 ≠ 0 → ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ ) )
14 11 13 sylbir ⊢ ( ¬ 𝑁 = 0 → ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ ) )
15 idd ⊢ ( ¬ 𝑁 = 0 → ( 𝐼 ∈ ℤ → 𝐼 ∈ ℤ ) )
16 10 14 15 3anim123d ⊢ ( ¬ 𝑁 = 0 → ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) ) )
17 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
18 17 anim2i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
19 repsw ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 )
20 18 19 syl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 )
21 cshword ⊢ ( ( ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) , ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ⟩ ) ++ ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ) ) )
22 20 21 stoic3 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) , ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ⟩ ) ++ ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ) ) )
23 repswlen ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )
24 18 23 syl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )
25 24 oveq2d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) = ( 𝐼 mod 𝑁 ) )
26 25 24 opeq12d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ⟨ ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) , ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ⟩ = ⟨ ( 𝐼 mod 𝑁 ) , 𝑁 ⟩ )
27 26 oveq2d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) , ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ⟩ ) = ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod 𝑁 ) , 𝑁 ⟩ ) )
28 25 oveq2d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ) = ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod 𝑁 ) ) )
29 27 28 oveq12d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) , ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ⟩ ) ++ ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ) ) = ( ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod 𝑁 ) , 𝑁 ⟩ ) ++ ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod 𝑁 ) ) ) )
30 29 3adant3 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) , ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ⟩ ) ++ ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ) ) = ( ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod 𝑁 ) , 𝑁 ⟩ ) ++ ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod 𝑁 ) ) ) )
31 18 3adant3 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
32 zmodcl ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐼 mod 𝑁 ) ∈ ℕ0 )
33 32 ancoms ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 mod 𝑁 ) ∈ ℕ0 )
34 17 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℕ0 )
35 33 34 jca ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝐼 mod 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
36 35 3adant1 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝐼 mod 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
37 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
38 37 leidd ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≤ 𝑁 )
39 38 3ad2ant2 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → 𝑁 ≤ 𝑁 )
40 repswswrd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ( 𝐼 mod 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑁 ) → ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod 𝑁 ) , 𝑁 ⟩ ) = ( 𝑆 repeatS ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ) )
41 31 36 39 40 syl3anc ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod 𝑁 ) , 𝑁 ⟩ ) = ( 𝑆 repeatS ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ) )
42 simp1 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → 𝑆 ∈ 𝑉 )
43 17 3ad2ant2 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℕ0 )
44 zmodfzp1 ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐼 mod 𝑁 ) ∈ ( 0 ... 𝑁 ) )
45 44 ancoms ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 mod 𝑁 ) ∈ ( 0 ... 𝑁 ) )
46 45 3adant1 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 mod 𝑁 ) ∈ ( 0 ... 𝑁 ) )
47 repswpfx ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐼 mod 𝑁 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod 𝑁 ) ) = ( 𝑆 repeatS ( 𝐼 mod 𝑁 ) ) )
48 42 43 46 47 syl3anc ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod 𝑁 ) ) = ( 𝑆 repeatS ( 𝐼 mod 𝑁 ) ) )
49 41 48 oveq12d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod 𝑁 ) , 𝑁 ⟩ ) ++ ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod 𝑁 ) ) ) = ( ( 𝑆 repeatS ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ) ++ ( 𝑆 repeatS ( 𝐼 mod 𝑁 ) ) ) )
50 32 nn0red ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐼 mod 𝑁 ) ∈ ℝ )
51 50 ancoms ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 mod 𝑁 ) ∈ ℝ )
52 37 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℝ )
53 zre ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
54 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
55 modlt ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( 𝐼 mod 𝑁 ) < 𝑁 )
56 53 54 55 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 mod 𝑁 ) < 𝑁 )
57 51 52 56 ltled ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 mod 𝑁 ) ≤ 𝑁 )
58 57 3adant1 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 mod 𝑁 ) ≤ 𝑁 )
59 33 3adant1 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 mod 𝑁 ) ∈ ℕ0 )
60 nn0sub ⊢ ( ( ( 𝐼 mod 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐼 mod 𝑁 ) ≤ 𝑁 ↔ ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ∈ ℕ0 ) )
61 59 43 60 syl2anc ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝐼 mod 𝑁 ) ≤ 𝑁 ↔ ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ∈ ℕ0 ) )
62 58 61 mpbid ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ∈ ℕ0 )
63 repswccat ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ∈ ℕ0 ∧ ( 𝐼 mod 𝑁 ) ∈ ℕ0 ) → ( ( 𝑆 repeatS ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ) ++ ( 𝑆 repeatS ( 𝐼 mod 𝑁 ) ) ) = ( 𝑆 repeatS ( ( 𝑁 − ( 𝐼 mod 𝑁 ) ) + ( 𝐼 mod 𝑁 ) ) ) )
64 42 62 59 63 syl3anc ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS ( 𝑁 − ( 𝐼 mod 𝑁 ) ) ) ++ ( 𝑆 repeatS ( 𝐼 mod 𝑁 ) ) ) = ( 𝑆 repeatS ( ( 𝑁 − ( 𝐼 mod 𝑁 ) ) + ( 𝐼 mod 𝑁 ) ) ) )
65 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
66 65 adantl ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
67 32 nn0cnd ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐼 mod 𝑁 ) ∈ ℂ )
68 66 67 npcand ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − ( 𝐼 mod 𝑁 ) ) + ( 𝐼 mod 𝑁 ) ) = 𝑁 )
69 68 ancoms ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝑁 − ( 𝐼 mod 𝑁 ) ) + ( 𝐼 mod 𝑁 ) ) = 𝑁 )
70 69 3adant1 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝑁 − ( 𝐼 mod 𝑁 ) ) + ( 𝐼 mod 𝑁 ) ) = 𝑁 )
71 70 oveq2d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( 𝑆 repeatS ( ( 𝑁 − ( 𝐼 mod 𝑁 ) ) + ( 𝐼 mod 𝑁 ) ) ) = ( 𝑆 repeatS 𝑁 ) )
72 49 64 71 3eqtrd ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( ( 𝑆 repeatS 𝑁 ) substr ⟨ ( 𝐼 mod 𝑁 ) , 𝑁 ⟩ ) ++ ( ( 𝑆 repeatS 𝑁 ) prefix ( 𝐼 mod 𝑁 ) ) ) = ( 𝑆 repeatS 𝑁 ) )
73 22 30 72 3eqtrd ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 𝑁 ) )
74 16 73 syl6 ⊢ ( ¬ 𝑁 = 0 → ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 𝑁 ) ) )
75 9 74 pm2.61i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( ( 𝑆 repeatS 𝑁 ) cyclShift 𝐼 ) = ( 𝑆 repeatS 𝑁 ) )