Metamath Proof Explorer


Theorem repswpfx

Description: A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020)

Ref Expression
Assertion repswpfx ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) = ( 𝑆 repeatS 𝐿 ) )

Proof

Step Hyp Ref Expression
1 repsw ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 )
2 1 3adant3 ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 )
3 repswlen ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )
4 3 oveq2d ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( 0 ... ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) = ( 0 ... 𝑁 ) )
5 4 eleq2d ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( 𝐿 ∈ ( 0 ... ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ↔ 𝐿 ∈ ( 0 ... 𝑁 ) ) )
6 5 biimp3ar ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) )
7 pfxlen ( ( ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ) → ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) = 𝐿 )
8 2 6 7 syl2anc ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) = 𝐿 )
9 elfznn0 ( 𝐿 ∈ ( 0 ... 𝑁 ) → 𝐿 ∈ ℕ0 )
10 repswlen ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 𝐿 ) ) = 𝐿 )
11 9 10 sylan2 ( ( 𝑆𝑉𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ ( 𝑆 repeatS 𝐿 ) ) = 𝐿 )
12 11 3adant2 ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ ( 𝑆 repeatS 𝐿 ) ) = 𝐿 )
13 8 12 eqtr4d ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) = ( ♯ ‘ ( 𝑆 repeatS 𝐿 ) ) )
14 simpl1 ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → 𝑆𝑉 )
15 simpl2 ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → 𝑁 ∈ ℕ0 )
16 elfzuz3 ( 𝐿 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ𝐿 ) )
17 16 3ad2ant3 ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ𝐿 ) )
18 8 fveq2d ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ℤ ‘ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) = ( ℤ𝐿 ) )
19 17 18 eleqtrrd ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ ‘ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) )
20 fzoss2 ( 𝑁 ∈ ( ℤ ‘ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
21 19 20 syl ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
22 21 sselda ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) )
23 repswsymb ( ( 𝑆𝑉𝑁 ∈ ℕ0𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑖 ) = 𝑆 )
24 14 15 22 23 syl3anc ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑖 ) = 𝑆 )
25 2 adantr ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 )
26 6 adantr ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) )
27 8 oveq2d ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) = ( 0 ..^ 𝐿 ) )
28 27 eleq2d ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ↔ 𝑖 ∈ ( 0 ..^ 𝐿 ) ) )
29 28 biimpa ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝐿 ) )
30 pfxfv ( ( ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝐿 ) ) → ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ‘ 𝑖 ) = ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑖 ) )
31 25 26 29 30 syl3anc ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ‘ 𝑖 ) = ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑖 ) )
32 9 3ad2ant3 ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → 𝐿 ∈ ℕ0 )
33 32 adantr ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → 𝐿 ∈ ℕ0 )
34 repswsymb ( ( 𝑆𝑉𝐿 ∈ ℕ0𝑖 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑆 repeatS 𝐿 ) ‘ 𝑖 ) = 𝑆 )
35 14 33 29 34 syl3anc ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → ( ( 𝑆 repeatS 𝐿 ) ‘ 𝑖 ) = 𝑆 )
36 24 31 35 3eqtr4d ( ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ) → ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ‘ 𝑖 ) = ( ( 𝑆 repeatS 𝐿 ) ‘ 𝑖 ) )
37 36 ralrimiva ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ‘ 𝑖 ) = ( ( 𝑆 repeatS 𝐿 ) ‘ 𝑖 ) )
38 pfxcl ( ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 → ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ∈ Word 𝑉 )
39 2 38 syl ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ∈ Word 𝑉 )
40 repsw ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉 )
41 9 40 sylan2 ( ( 𝑆𝑉𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉 )
42 eqwrd ( ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ∈ Word 𝑉 ∧ ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉 ) → ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) = ( 𝑆 repeatS 𝐿 ) ↔ ( ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) = ( ♯ ‘ ( 𝑆 repeatS 𝐿 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ‘ 𝑖 ) = ( ( 𝑆 repeatS 𝐿 ) ‘ 𝑖 ) ) ) )
43 39 41 42 3imp3i2an ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) = ( 𝑆 repeatS 𝐿 ) ↔ ( ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) = ( ♯ ‘ ( 𝑆 repeatS 𝐿 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ) ) ( ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) ‘ 𝑖 ) = ( ( 𝑆 repeatS 𝐿 ) ‘ 𝑖 ) ) ) )
44 13 37 43 mpbir2and ( ( 𝑆𝑉𝑁 ∈ ℕ0𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) prefix 𝐿 ) = ( 𝑆 repeatS 𝐿 ) )