Step | Hyp | Ref
| Expression |
1 | | repsw 13891 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
2 | 1 | 3adant3 1168 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
3 | | repswlen 13892 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(♯‘(𝑆 repeatS
𝑁)) = 𝑁) |
4 | 3 | eqcomd 2831 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝑁 = (♯‘(𝑆 repeatS 𝑁))) |
5 | 4 | oveq2d 6921 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(0...𝑁) =
(0...(♯‘(𝑆
repeatS 𝑁)))) |
6 | 5 | eleq2d 2892 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐿 ∈ (0...𝑁) ↔ 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁))))) |
7 | 6 | biimp3a 1599 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁)))) |
8 | | pfxlen 13762 |
. . . 4
⊢ (((𝑆 repeatS 𝑁) ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁)))) → (♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = 𝐿) |
9 | 2, 7, 8 | syl2anc 581 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = 𝐿) |
10 | | elfznn0 12727 |
. . . . . 6
⊢ (𝐿 ∈ (0...𝑁) → 𝐿 ∈
ℕ0) |
11 | 10 | anim2i 612 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 ∈ 𝑉 ∧ 𝐿 ∈
ℕ0)) |
12 | 11 | 3adant2 1167 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 ∈ 𝑉 ∧ 𝐿 ∈
ℕ0)) |
13 | | repswlen 13892 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) →
(♯‘(𝑆 repeatS
𝐿)) = 𝐿) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (♯‘(𝑆 repeatS 𝐿)) = 𝐿) |
15 | 9, 14 | eqtr4d 2864 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (♯‘(𝑆 repeatS 𝐿))) |
16 | | simpl1 1248 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑆 ∈ 𝑉) |
17 | | simpl2 1250 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑁 ∈
ℕ0) |
18 | | elfzuz3 12632 |
. . . . . . . . 9
⊢ (𝐿 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝐿)) |
19 | 18 | 3ad2ant3 1171 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐿)) |
20 | 9 | fveq2d 6437 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) →
(ℤ≥‘(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) = (ℤ≥‘𝐿)) |
21 | 19, 20 | eleqtrrd 2909 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝑁 ∈
(ℤ≥‘(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) |
22 | | fzoss2 12791 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) → (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) ⊆ (0..^𝑁)) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) ⊆ (0..^𝑁)) |
24 | 23 | sselda 3827 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑖 ∈ (0..^𝑁)) |
25 | | repswsymb 13890 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘𝑖) = 𝑆) |
26 | 16, 17, 24, 25 | syl3anc 1496 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → ((𝑆 repeatS 𝑁)‘𝑖) = 𝑆) |
27 | 2 | adantr 474 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
28 | 7 | adantr 474 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁)))) |
29 | 9 | oveq2d 6921 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) = (0..^𝐿)) |
30 | 29 | eleq2d 2892 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿))) ↔ 𝑖 ∈ (0..^𝐿))) |
31 | 30 | biimpa 470 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝑖 ∈ (0..^𝐿)) |
32 | | pfxfv 13761 |
. . . . 5
⊢ (((𝑆 repeatS 𝑁) ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘(𝑆 repeatS 𝑁))) ∧ 𝑖 ∈ (0..^𝐿)) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝑁)‘𝑖)) |
33 | 27, 28, 31, 32 | syl3anc 1496 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝑁)‘𝑖)) |
34 | 10 | 3ad2ant3 1171 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → 𝐿 ∈
ℕ0) |
35 | 34 | adantr 474 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → 𝐿 ∈
ℕ0) |
36 | | repswsymb 13890 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ 𝑖 ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘𝑖) = 𝑆) |
37 | 16, 35, 31, 36 | syl3anc 1496 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → ((𝑆 repeatS 𝐿)‘𝑖) = 𝑆) |
38 | 26, 33, 37 | 3eqtr4d 2871 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) ∧ 𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))) → (((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)) |
39 | 38 | ralrimiva 3175 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ∀𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)) |
40 | | pfxcl 13756 |
. . . 4
⊢ ((𝑆 repeatS 𝑁) ∈ Word 𝑉 → ((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉) |
41 | 2, 40 | syl 17 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉) |
42 | | repsw 13891 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉) |
43 | 12, 42 | syl 17 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (𝑆 repeatS 𝐿) ∈ Word 𝑉) |
44 | | eqwrd 13617 |
. . 3
⊢ ((((𝑆 repeatS 𝑁) prefix 𝐿) ∈ Word 𝑉 ∧ (𝑆 repeatS 𝐿) ∈ Word 𝑉) → (((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿) ↔ ((♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (♯‘(𝑆 repeatS 𝐿)) ∧ ∀𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)))) |
45 | 41, 43, 44 | syl2anc 581 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → (((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿) ↔ ((♯‘((𝑆 repeatS 𝑁) prefix 𝐿)) = (♯‘(𝑆 repeatS 𝐿)) ∧ ∀𝑖 ∈ (0..^(♯‘((𝑆 repeatS 𝑁) prefix 𝐿)))(((𝑆 repeatS 𝑁) prefix 𝐿)‘𝑖) = ((𝑆 repeatS 𝐿)‘𝑖)))) |
46 | 15, 39, 45 | mpbir2and 706 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿)) |