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