Step | Hyp | Ref
| Expression |
1 | | eqwrd 13346 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) → (𝑊 = 𝑆 ↔ ((#‘𝑊) = (#‘𝑆) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)))) |
2 | 1 | 3adant3 1081 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 = 𝑆 ↔ ((#‘𝑊) = (#‘𝑆) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)))) |
3 | | elfzofz 12485 |
. . . . . . . . 9
⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ (0...(#‘𝑊))) |
4 | | fzosplit 12501 |
. . . . . . . . 9
⊢ (𝐼 ∈ (0...(#‘𝑊)) → (0..^(#‘𝑊)) = ((0..^𝐼) ∪ (𝐼..^(#‘𝑊)))) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (𝐼 ∈ (0..^(#‘𝑊)) → (0..^(#‘𝑊)) = ((0..^𝐼) ∪ (𝐼..^(#‘𝑊)))) |
6 | 5 | 3ad2ant3 1084 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (0..^(#‘𝑊)) = ((0..^𝐼) ∪ (𝐼..^(#‘𝑊)))) |
7 | 6 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (0..^(#‘𝑊)) = ((0..^𝐼) ∪ (𝐼..^(#‘𝑊)))) |
8 | 7 | raleqdv 3144 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ ∀𝑖 ∈ ((0..^𝐼) ∪ (𝐼..^(#‘𝑊)))(𝑊‘𝑖) = (𝑆‘𝑖))) |
9 | | ralunb 3794 |
. . . . 5
⊢
(∀𝑖 ∈
((0..^𝐼) ∪ (𝐼..^(#‘𝑊)))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ∧ ∀𝑖 ∈ (𝐼..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖))) |
10 | 8, 9 | syl6bb 276 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ∧ ∀𝑖 ∈ (𝐼..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)))) |
11 | | 3simpa 1058 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉)) |
12 | 11 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉)) |
13 | | elfzonn0 12512 |
. . . . . . . . 9
⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈
ℕ0) |
14 | 13 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝐼 ∈
ℕ0) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → 𝐼 ∈
ℕ0) |
16 | | 0nn0 11307 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
17 | 15, 16 | jctil 560 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (0 ∈ ℕ0
∧ 𝐼 ∈
ℕ0)) |
18 | | elfzo0le 12511 |
. . . . . . . 8
⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ≤ (#‘𝑊)) |
19 | 18 | 3ad2ant3 1084 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝐼 ≤ (#‘𝑊)) |
20 | 19 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → 𝐼 ≤ (#‘𝑊)) |
21 | | breq2 4657 |
. . . . . . . 8
⊢
((#‘𝑊) =
(#‘𝑆) → (𝐼 ≤ (#‘𝑊) ↔ 𝐼 ≤ (#‘𝑆))) |
22 | 21 | adantl 482 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (𝐼 ≤ (#‘𝑊) ↔ 𝐼 ≤ (#‘𝑆))) |
23 | 20, 22 | mpbid 222 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → 𝐼 ≤ (#‘𝑆)) |
24 | | swrdspsleq 13449 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) ∧ (0 ∈ ℕ0 ∧
𝐼 ∈
ℕ0) ∧ (𝐼 ≤ (#‘𝑊) ∧ 𝐼 ≤ (#‘𝑆))) → ((𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉) ↔ ∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖))) |
25 | 24 | bicomd 213 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) ∧ (0 ∈ ℕ0 ∧
𝐼 ∈
ℕ0) ∧ (𝐼 ≤ (#‘𝑊) ∧ 𝐼 ≤ (#‘𝑆))) → (∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉))) |
26 | 12, 17, 20, 23, 25 | syl112anc 1330 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉))) |
27 | | lencl 13324 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
28 | 27 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (#‘𝑊) ∈
ℕ0) |
29 | 14, 28 | jca 554 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝐼 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0)) |
30 | 29 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (𝐼 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0)) |
31 | | nn0re 11301 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℝ) |
32 | 31 | leidd 10594 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ≤ (#‘𝑊)) |
33 | 27, 32 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ≤ (#‘𝑊)) |
34 | 33 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (#‘𝑊) ≤ (#‘𝑊)) |
35 | 34 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (#‘𝑊) ≤ (#‘𝑊)) |
36 | | breq2 4657 |
. . . . . . . 8
⊢
((#‘𝑊) =
(#‘𝑆) →
((#‘𝑊) ≤
(#‘𝑊) ↔
(#‘𝑊) ≤
(#‘𝑆))) |
37 | 36 | adantl 482 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → ((#‘𝑊) ≤ (#‘𝑊) ↔ (#‘𝑊) ≤ (#‘𝑆))) |
38 | 35, 37 | mpbid 222 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (#‘𝑊) ≤ (#‘𝑆)) |
39 | | swrdspsleq 13449 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) ∧ (𝐼 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0) ∧ ((#‘𝑊) ≤ (#‘𝑊) ∧ (#‘𝑊) ≤ (#‘𝑆))) → ((𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉) ↔ ∀𝑖 ∈ (𝐼..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖))) |
40 | 39 | bicomd 213 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉) ∧ (𝐼 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0) ∧ ((#‘𝑊) ≤ (#‘𝑊) ∧ (#‘𝑊) ≤ (#‘𝑆))) → (∀𝑖 ∈ (𝐼..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉))) |
41 | 12, 30, 35, 38, 40 | syl112anc 1330 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (∀𝑖 ∈ (𝐼..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ (𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉))) |
42 | 26, 41 | anbi12d 747 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → ((∀𝑖 ∈ (0..^𝐼)(𝑊‘𝑖) = (𝑆‘𝑖) ∧ ∀𝑖 ∈ (𝐼..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)) ↔ ((𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉) ∧ (𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉)))) |
43 | 10, 42 | bitrd 268 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) ∧ (#‘𝑊) = (#‘𝑆)) → (∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖) ↔ ((𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉) ∧ (𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉)))) |
44 | 43 | pm5.32da 673 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) = (#‘𝑆) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑆‘𝑖)) ↔ ((#‘𝑊) = (#‘𝑆) ∧ ((𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉) ∧ (𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉))))) |
45 | 2, 44 | bitrd 268 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 = 𝑆 ↔ ((#‘𝑊) = (#‘𝑆) ∧ ((𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉) ∧ (𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉))))) |