Step | Hyp | Ref
| Expression |
1 | | repsw 13373 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
2 | 1 | 3adant3 1074 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
3 | | repswlen 13374 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑆 repeatS 𝑁)) = 𝑁) |
4 | 3 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝑁 = (#‘(𝑆 repeatS 𝑁))) |
5 | 4 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(0...𝑁) =
(0...(#‘(𝑆 repeatS
𝑁)))) |
6 | 5 | eleq2d 2673 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐿 ∈ (0...𝑁) ↔ 𝐿 ∈ (0...(#‘(𝑆 repeatS 𝑁))))) |
7 | 6 | biimp3a 1424 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝐿 ∈ (0...(#‘(𝑆 repeatS 𝑁)))) |
8 | | pfxlen 40254 |
. . . 4
⊢ (((𝑆 repeatS 𝑁) ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘(𝑆 repeatS 𝑁)))) → (#‘((𝑆 repeatS 𝑁) prefix 𝐿)) = 𝐿) |
9 | 2, 7, 8 | syl2anc 691 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (#‘((𝑆 repeatS 𝑁) prefix 𝐿)) = 𝐿) |
10 | | elfznn0 12302 |
. . . . . 6
⊢ (𝐿 ∈ (0...𝑁) → 𝐿 ∈
ℕ0) |
11 | 10 | anim2i 591 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 ∈ 𝑉 ∧ 𝐿 ∈
ℕ0)) |
12 | 11 | 3adant2 1073 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 ∈ 𝑉 ∧ 𝐿 ∈
ℕ0)) |
13 | | repswlen 13374 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) →
(#‘(𝑆 repeatS 𝐿)) = 𝐿) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (#‘(𝑆 repeatS 𝐿)) = 𝐿) |
15 | 9, 14 | eqtr4d 2647 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (#‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (#‘(𝑆 repeatS 𝐿))) |
16 | | simpl1 1057 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑆 ∈ 𝑉) |
17 | | simpl2 1058 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑁 ∈
ℕ0) |
18 | | elfzuz3 12210 |
. . . . . . . . 9
⊢ (𝐿 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝐿)) |
19 | 18 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐿)) |
20 | 9 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) →
(ℤ≥‘(#‘((𝑆 repeatS 𝑁) prefix 𝐿))) = (ℤ≥‘𝐿)) |
21 | 19, 20 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝑁 ∈
(ℤ≥‘(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) |
22 | | fzoss2 12365 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘(#‘((𝑆 repeatS 𝑁) prefix 𝐿))) → (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿))) ⊆ (0..^𝑁)) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿))) ⊆ (0..^𝑁)) |
24 | 23 | sselda 3568 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑖 ∈ (0..^𝑁)) |
25 | | repswsymb 13372 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘𝑖) = 𝑆) |
26 | 16, 17, 24, 25 | syl3anc 1318 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → ((𝑆 repeatS 𝑁)‘𝑖) = 𝑆) |
27 | 2 | adantr 480 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
28 | 7 | adantr 480 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝐿 ∈ (0...(#‘(𝑆 repeatS 𝑁)))) |
29 | 9 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿))) = (0..^𝐿)) |
30 | 29 | eleq2d 2673 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿))) ↔ 𝑖 ∈ (0..^𝐿))) |
31 | 30 | biimpa 500 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑖 ∈ (0..^𝐿)) |
32 | | pfxfv 40262 |
. . . . 5
⊢ (((𝑆 repeatS 𝑁) ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘(𝑆 repeatS 𝑁))) ∧ 𝑖 ∈ (0..^𝐿)) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝑁)‘𝑖)) |
33 | 27, 28, 31, 32 | syl3anc 1318 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝑁)‘𝑖)) |
34 | 10 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝐿 ∈
ℕ0) |
35 | 34 | adantr 480 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝐿 ∈
ℕ0) |
36 | | repswsymb 13372 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ 𝑖 ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘𝑖) = 𝑆) |
37 | 16, 35, 31, 36 | syl3anc 1318 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → ((𝑆 repeatS 𝐿)‘𝑖) = 𝑆) |
38 | 26, 33, 37 | 3eqtr4d 2654 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)) |
39 | 38 | ralrimiva 2949 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ∀𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)) |
40 | | pfxcl 40249 |
. . . 4
⊢ ((𝑆 repeatS 𝑁) ∈ Word 𝑉 → ((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉) |
41 | 2, 40 | syl 17 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉) |
42 | | repsw 13373 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉) |
43 | 12, 42 | syl 17 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 repeatS 𝐿) ∈ Word 𝑉) |
44 | | eqwrd 13201 |
. . 3
⊢ ((((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉 ∧ (𝑆 repeatS 𝐿) ∈ Word 𝑉) → (((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿) ↔ ((#‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (#‘(𝑆 repeatS 𝐿)) ∧ ∀𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)))) |
45 | 41, 43, 44 | syl2anc 691 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿) ↔ ((#‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (#‘(𝑆 repeatS 𝐿)) ∧ ∀𝑖 ∈ (0..^(#‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)))) |
46 | 15, 39, 45 | mpbir2and 959 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿)) |