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 𝐿 ) )