Proof of Theorem swrdeq
Step | Hyp | Ref
| Expression |
1 | | swrdcl 13271 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈0, 𝑀〉) ∈ Word 𝑉) |
2 | | swrdcl 13271 |
. . . . 5
⊢ (𝑈 ∈ Word 𝑉 → (𝑈 substr 〈0, 𝑁〉) ∈ Word 𝑉) |
3 | 1, 2 | anim12i 588 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → ((𝑊 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ (𝑈 substr 〈0, 𝑁〉) ∈ Word 𝑉)) |
4 | 3 | 3ad2ant1 1075 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ (𝑈 substr 〈0, 𝑁〉) ∈ Word 𝑉)) |
5 | | eqwrd 13201 |
. . 3
⊢ (((𝑊 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ (𝑈 substr 〈0, 𝑁〉) ∈ Word 𝑉) → ((𝑊 substr 〈0, 𝑀〉) = (𝑈 substr 〈0, 𝑁〉) ↔ ((#‘(𝑊 substr 〈0, 𝑀〉)) = (#‘(𝑈 substr 〈0, 𝑁〉)) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 substr 〈0, 𝑀〉)))((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖)))) |
6 | 4, 5 | syl 17 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 substr 〈0, 𝑀〉) = (𝑈 substr 〈0, 𝑁〉) ↔ ((#‘(𝑊 substr 〈0, 𝑀〉)) = (#‘(𝑈 substr 〈0, 𝑁〉)) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 substr 〈0, 𝑀〉)))((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖)))) |
7 | | simpl 472 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉) |
8 | 7 | 3ad2ant1 1075 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑊 ∈ Word 𝑉) |
9 | | simpl 472 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑀 ∈
ℕ0) |
10 | 9 | 3ad2ant2 1076 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑀 ∈
ℕ0) |
11 | | lencl 13179 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (#‘𝑊) ∈
ℕ0) |
13 | 12 | 3ad2ant1 1075 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘𝑊) ∈
ℕ0) |
14 | | simpl 472 |
. . . . . . 7
⊢ ((𝑀 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)) → 𝑀 ≤ (#‘𝑊)) |
15 | 14 | 3ad2ant3 1077 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑀 ≤ (#‘𝑊)) |
16 | | elfz2nn0 12300 |
. . . . . 6
⊢ (𝑀 ∈ (0...(#‘𝑊)) ↔ (𝑀 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑀
≤ (#‘𝑊))) |
17 | 10, 13, 15, 16 | syl3anbrc 1239 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑀 ∈ (0...(#‘𝑊))) |
18 | | swrd0len 13274 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈0, 𝑀〉)) = 𝑀) |
19 | 8, 17, 18 | syl2anc 691 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘(𝑊 substr 〈0, 𝑀〉)) = 𝑀) |
20 | | simpr 476 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → 𝑈 ∈ Word 𝑉) |
21 | 20 | 3ad2ant1 1075 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑈 ∈ Word 𝑉) |
22 | | simpr 476 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
23 | 22 | 3ad2ant2 1076 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑁 ∈
ℕ0) |
24 | | lencl 13179 |
. . . . . . . 8
⊢ (𝑈 ∈ Word 𝑉 → (#‘𝑈) ∈
ℕ0) |
25 | 24 | adantl 481 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (#‘𝑈) ∈
ℕ0) |
26 | 25 | 3ad2ant1 1075 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘𝑈) ∈
ℕ0) |
27 | | simpr 476 |
. . . . . . 7
⊢ ((𝑀 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)) → 𝑁 ≤ (#‘𝑈)) |
28 | 27 | 3ad2ant3 1077 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑁 ≤ (#‘𝑈)) |
29 | | elfz2nn0 12300 |
. . . . . 6
⊢ (𝑁 ∈ (0...(#‘𝑈)) ↔ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑈))) |
30 | 23, 26, 28, 29 | syl3anbrc 1239 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑁 ∈ (0...(#‘𝑈))) |
31 | | swrd0len 13274 |
. . . . 5
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈))) → (#‘(𝑈 substr 〈0, 𝑁〉)) = 𝑁) |
32 | 21, 30, 31 | syl2anc 691 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘(𝑈 substr 〈0, 𝑁〉)) = 𝑁) |
33 | 19, 32 | eqeq12d 2625 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((#‘(𝑊 substr 〈0, 𝑀〉)) = (#‘(𝑈 substr 〈0, 𝑁〉)) ↔ 𝑀 = 𝑁)) |
34 | 33 | anbi1d 737 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (((#‘(𝑊 substr 〈0, 𝑀〉)) = (#‘(𝑈 substr 〈0, 𝑁〉)) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 substr 〈0, 𝑀〉)))((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 substr 〈0, 𝑀〉)))((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖)))) |
35 | 8 | adantr 480 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → 𝑊 ∈ Word 𝑉) |
36 | 17 | adantr 480 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → 𝑀 ∈ (0...(#‘𝑊))) |
37 | 35, 36, 18 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (#‘(𝑊 substr 〈0, 𝑀〉)) = 𝑀) |
38 | 37 | oveq2d 6565 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (0..^(#‘(𝑊 substr 〈0, 𝑀〉))) = (0..^𝑀)) |
39 | 38 | raleqdv 3121 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^(#‘(𝑊 substr 〈0, 𝑀〉)))((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖))) |
40 | 35 | adantr 480 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ Word 𝑉) |
41 | 36 | adantr 480 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ (0...(#‘𝑊))) |
42 | | simpr 476 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀)) |
43 | | swrd0fv 13291 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊)) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑊 substr 〈0, 𝑀〉)‘𝑖) = (𝑊‘𝑖)) |
44 | 40, 41, 42, 43 | syl3anc 1318 |
. . . . . 6
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑊 substr 〈0, 𝑀〉)‘𝑖) = (𝑊‘𝑖)) |
45 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁)) |
46 | 45 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝑀 = 𝑁 → (𝑖 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑁))) |
47 | 46 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (𝑖 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑁))) |
48 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑈 ∈ Word 𝑉) |
49 | 30 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑁 ∈ (0...(#‘𝑈))) |
50 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^𝑁)) |
51 | 48, 49, 50 | 3jca 1235 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁))) |
52 | 51 | ex 449 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (𝑖 ∈ (0..^𝑁) → (𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁)))) |
53 | 52 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (𝑖 ∈ (0..^𝑁) → (𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁)))) |
54 | 47, 53 | sylbid 229 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (𝑖 ∈ (0..^𝑀) → (𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁)))) |
55 | 54 | imp 444 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁))) |
56 | | swrd0fv 13291 |
. . . . . . 7
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑈 substr 〈0, 𝑁〉)‘𝑖) = (𝑈‘𝑖)) |
57 | 55, 56 | syl 17 |
. . . . . 6
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑈 substr 〈0, 𝑁〉)‘𝑖) = (𝑈‘𝑖)) |
58 | 44, 57 | eqeq12d 2625 |
. . . . 5
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖) ↔ (𝑊‘𝑖) = (𝑈‘𝑖))) |
59 | 58 | ralbidva 2968 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^𝑀)((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))) |
60 | 39, 59 | bitrd 267 |
. . 3
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^(#‘(𝑊 substr 〈0, 𝑀〉)))((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))) |
61 | 60 | pm5.32da 671 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 substr 〈0, 𝑀〉)))((𝑊 substr 〈0, 𝑀〉)‘𝑖) = ((𝑈 substr 〈0, 𝑁〉)‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |
62 | 6, 34, 61 | 3bitrd 293 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 substr 〈0, 𝑀〉) = (𝑈 substr 〈0, 𝑁〉) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |