Step | Hyp | Ref
| Expression |
1 | | eqwrd 13647 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) → (𝑊 = 𝑆 ↔ ((♯‘𝑊) = (♯‘𝑆) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)))) |
2 | 1 | 3adant3 1123 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 = 𝑆 ↔ ((♯‘𝑊) = (♯‘𝑆) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)))) |
3 | | elfzofz 12804 |
. . . . . . . . 9
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ 𝐼 ∈
(0...(♯‘𝑊))) |
4 | | fzosplit 12820 |
. . . . . . . . 9
⊢ (𝐼 ∈
(0...(♯‘𝑊))
→ (0..^(♯‘𝑊)) = ((0..^𝐼) ∪ (𝐼..^(♯‘𝑊)))) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (0..^(♯‘𝑊)) = ((0..^𝐼) ∪ (𝐼..^(♯‘𝑊)))) |
6 | 5 | 3ad2ant3 1126 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) →
(0..^(♯‘𝑊)) =
((0..^𝐼) ∪ (𝐼..^(♯‘𝑊)))) |
7 | 6 | adantr 474 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) →
(0..^(♯‘𝑊)) =
((0..^𝐼) ∪ (𝐼..^(♯‘𝑊)))) |
8 | 7 | raleqdv 3339 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ ∀𝑖 ∈ ((0..^𝐼) ∪ (𝐼..^(♯‘𝑊)))(𝑊‘𝑖) = (𝑆‘𝑖))) |
9 | | ralunb 4016 |
. . . . 5
⊢
(∀𝑖 ∈
((0..^𝐼) ∪ (𝐼..^(♯‘𝑊)))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ∧ ∀𝑖 ∈ (𝐼..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖))) |
10 | 8, 9 | syl6bb 279 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ∧ ∀𝑖 ∈ (𝐼..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)))) |
11 | | eqidd 2778 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → 𝐼 = 𝐼) |
12 | 11 | biantrurd 528 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (𝐼 = 𝐼 ∧ ∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖)))) |
13 | | 3simpa 1139 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉)) |
14 | 13 | adantr 474 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉)) |
15 | | elfzonn0 12832 |
. . . . . . . . . 10
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ 𝐼 ∈
ℕ0) |
16 | 15, 15 | jca 507 |
. . . . . . . . 9
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝐼 ∈
ℕ0 ∧ 𝐼
∈ ℕ0)) |
17 | 16 | 3ad2ant3 1126 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝐼 ∈ ℕ0 ∧ 𝐼 ∈
ℕ0)) |
18 | 17 | adantr 474 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (𝐼 ∈ ℕ0 ∧ 𝐼 ∈
ℕ0)) |
19 | | elfzo0le 12831 |
. . . . . . . . 9
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ 𝐼 ≤
(♯‘𝑊)) |
20 | 19 | 3ad2ant3 1126 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → 𝐼 ≤ (♯‘𝑊)) |
21 | 20 | adantr 474 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → 𝐼 ≤ (♯‘𝑊)) |
22 | | breq2 4890 |
. . . . . . . . . 10
⊢
((♯‘𝑆) =
(♯‘𝑊) →
(𝐼 ≤
(♯‘𝑆) ↔
𝐼 ≤ (♯‘𝑊))) |
23 | 22 | eqcoms 2785 |
. . . . . . . . 9
⊢
((♯‘𝑊) =
(♯‘𝑆) →
(𝐼 ≤
(♯‘𝑆) ↔
𝐼 ≤ (♯‘𝑊))) |
24 | 23 | adantl 475 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (𝐼 ≤ (♯‘𝑆) ↔ 𝐼 ≤ (♯‘𝑊))) |
25 | 21, 24 | mpbird 249 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → 𝐼 ≤ (♯‘𝑆)) |
26 | | pfxeq 13805 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) ∧ (𝐼 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0)
∧ (𝐼 ≤
(♯‘𝑊) ∧
𝐼 ≤ (♯‘𝑆))) → ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ↔ (𝐼 = 𝐼 ∧ ∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖)))) |
27 | 14, 18, 21, 25, 26 | syl112anc 1442 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ↔ (𝐼 = 𝐼 ∧ ∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖)))) |
28 | 12, 27 | bitr4d 274 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (𝑊 prefix 𝐼) = (𝑆 prefix 𝐼))) |
29 | | lencl 13621 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
30 | 29, 15 | anim12i 606 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℕ0
∧ 𝐼 ∈
ℕ0)) |
31 | 30 | 3adant2 1122 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℕ0
∧ 𝐼 ∈
ℕ0)) |
32 | 31 | ancomd 455 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝐼 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ0)) |
33 | 32 | adantr 474 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (𝐼 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ0)) |
34 | 29 | nn0red 11703 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℝ) |
35 | 34 | leidd 10941 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ≤ (♯‘𝑊)) |
36 | 35 | 3ad2ant1 1124 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (♯‘𝑊) ≤ (♯‘𝑊)) |
37 | 36 | adantr 474 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (♯‘𝑊) ≤ (♯‘𝑊)) |
38 | 34 | 3ad2ant1 1124 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (♯‘𝑊) ∈
ℝ) |
39 | | eqle 10478 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℝ ∧ (♯‘𝑊) = (♯‘𝑆)) → (♯‘𝑊) ≤ (♯‘𝑆)) |
40 | 38, 39 | sylan 575 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (♯‘𝑊) ≤ (♯‘𝑆)) |
41 | | swrdspsleq 13769 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) ∧ (𝐼 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ0) ∧ ((♯‘𝑊) ≤ (♯‘𝑊) ∧ (♯‘𝑊) ≤ (♯‘𝑆))) → ((𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉) ↔ ∀𝑖 ∈ (𝐼..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖))) |
42 | 41 | bicomd 215 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) ∧ (𝐼 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ0) ∧ ((♯‘𝑊) ≤ (♯‘𝑊) ∧ (♯‘𝑊) ≤ (♯‘𝑆))) → (∀𝑖 ∈ (𝐼..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉))) |
43 | 14, 33, 37, 40, 42 | syl112anc 1442 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (∀𝑖 ∈ (𝐼..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉))) |
44 | 28, 43 | anbi12d 624 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → ((∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ∧ ∀𝑖 ∈ (𝐼..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)) ↔ ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ∧ (𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉)))) |
45 | 10, 44 | bitrd 271 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) ∧ (♯‘𝑊) = (♯‘𝑆)) → (∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ∧ (𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉)))) |
46 | 45 | pm5.32da 574 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) →
(((♯‘𝑊) =
(♯‘𝑆) ∧
∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)) ↔ ((♯‘𝑊) = (♯‘𝑆) ∧ ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ∧ (𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉))))) |
47 | 2, 46 | bitrd 271 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 = 𝑆 ↔ ((♯‘𝑊) = (♯‘𝑆) ∧ ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ∧ (𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉))))) |