Step | Hyp | Ref
| Expression |
1 | | repsw 14238 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
2 | 1 | 3adant3 1133 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
3 | | repswlen 14239 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(♯‘(𝑆 repeatS
𝑁)) = 𝑁) |
4 | 3 | oveq2d 7198 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(0...(♯‘(𝑆
repeatS 𝑁))) = (0...𝑁)) |
5 | 4 | eleq2d 2819 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐿 ∈
(0...(♯‘(𝑆
repeatS 𝑁))) ↔ 𝐿 ∈ (0...𝑁))) |
6 | 5 | biimp3ar 1471 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁)))) |
7 | | pfxlen 14146 |
. . . 4
⊢ (((𝑆 repeatS 𝑁) ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁)))) → (♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = 𝐿) |
8 | 2, 6, 7 | syl2anc 587 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = 𝐿) |
9 | | elfznn0 13103 |
. . . . 5
⊢ (𝐿 ∈ (0...𝑁) → 𝐿 ∈
ℕ0) |
10 | | repswlen 14239 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) →
(♯‘(𝑆 repeatS
𝐿)) = 𝐿) |
11 | 9, 10 | sylan2 596 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ (0...𝑁)) → (♯‘(𝑆 repeatS 𝐿)) = 𝐿) |
12 | 11 | 3adant2 1132 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (♯‘(𝑆 repeatS 𝐿)) = 𝐿) |
13 | 8, 12 | eqtr4d 2777 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (♯‘(𝑆 repeatS 𝐿))) |
14 | | simpl1 1192 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑆 ∈ 𝑉) |
15 | | simpl2 1193 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑁 ∈
ℕ0) |
16 | | elfzuz3 13007 |
. . . . . . . . 9
⊢ (𝐿 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝐿)) |
17 | 16 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐿)) |
18 | 8 | fveq2d 6690 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) →
(ℤ≥‘(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) = (ℤ≥‘𝐿)) |
19 | 17, 18 | eleqtrrd 2837 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝑁 ∈
(ℤ≥‘(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) |
20 | | fzoss2 13168 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) → (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) ⊆ (0..^𝑁)) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) ⊆ (0..^𝑁)) |
22 | 21 | sselda 3887 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑖 ∈ (0..^𝑁)) |
23 | | repswsymb 14237 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘𝑖) = 𝑆) |
24 | 14, 15, 22, 23 | syl3anc 1372 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → ((𝑆 repeatS 𝑁)‘𝑖) = 𝑆) |
25 | 2 | adantr 484 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
26 | 6 | adantr 484 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁)))) |
27 | 8 | oveq2d 7198 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) = (0..^𝐿)) |
28 | 27 | eleq2d 2819 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) ↔ 𝑖 ∈ (0..^𝐿))) |
29 | 28 | biimpa 480 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑖 ∈ (0..^𝐿)) |
30 | | pfxfv 14145 |
. . . . 5
⊢ (((𝑆 repeatS 𝑁) ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁))) ∧ 𝑖 ∈ (0..^𝐿)) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝑁)‘𝑖)) |
31 | 25, 26, 29, 30 | syl3anc 1372 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝑁)‘𝑖)) |
32 | 9 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝐿 ∈
ℕ0) |
33 | 32 | adantr 484 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝐿 ∈
ℕ0) |
34 | | repswsymb 14237 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ 𝑖 ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘𝑖) = 𝑆) |
35 | 14, 33, 29, 34 | syl3anc 1372 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → ((𝑆 repeatS 𝐿)‘𝑖) = 𝑆) |
36 | 24, 31, 35 | 3eqtr4d 2784 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)) |
37 | 36 | ralrimiva 3097 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ∀𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)) |
38 | | pfxcl 14140 |
. . . 4
⊢ ((𝑆 repeatS 𝑁) ∈ Word 𝑉 → ((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉) |
39 | 2, 38 | syl 17 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉) |
40 | | repsw 14238 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉) |
41 | 9, 40 | sylan2 596 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 repeatS 𝐿) ∈ Word 𝑉) |
42 | | eqwrd 14010 |
. . 3
⊢ ((((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉 ∧ (𝑆 repeatS 𝐿) ∈ Word 𝑉) → (((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿) ↔ ((♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (♯‘(𝑆 repeatS 𝐿)) ∧ ∀𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)))) |
43 | 39, 41, 42 | 3imp3i2an 1346 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿) ↔ ((♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (♯‘(𝑆 repeatS 𝐿)) ∧ ∀𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)))) |
44 | 13, 37, 43 | mpbir2and 713 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿)) |