Proof of Theorem clwlkf1clwwlklem
Step | Hyp | Ref
| Expression |
1 | | clwlkfclwwlk.1 |
. . . . . . . . . . . . 13
⊢ 𝐴 = (1st ‘𝑐) |
2 | | clwlkfclwwlk.2 |
. . . . . . . . . . . . 13
⊢ 𝐵 = (2nd ‘𝑐) |
3 | | clwlkfclwwlk.c |
. . . . . . . . . . . . 13
⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} |
4 | | clwlkfclwwlk.f |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) |
5 | 1, 2, 3, 4 | clwlkf1clwwlklem3 26375 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ 𝐶 → (2nd ‘𝑊) ∈ Word 𝑉) |
6 | 1, 2, 3, 4 | clwlkf1clwwlklem3 26375 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝐶 → (2nd ‘𝑈) ∈ Word 𝑉) |
7 | 5, 6 | anim12ci 589 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) → ((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉)) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) ∧ 𝑁 ∈ ℕ) → ((2nd
‘𝑈) ∈ Word 𝑉 ∧ (2nd
‘𝑊) ∈ Word 𝑉)) |
9 | | nnnn0 11176 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
10 | 9 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) |
11 | 1, 2, 3, 4 | clwlkf1clwwlklem1 26373 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ 𝐶 → 𝑁 ≤ (#‘(2nd ‘𝑈))) |
12 | 11 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) → 𝑁 ≤ (#‘(2nd ‘𝑈))) |
13 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) ∧ 𝑁 ∈ ℕ) → 𝑁 ≤ (#‘(2nd ‘𝑈))) |
14 | 1, 2, 3, 4 | clwlkf1clwwlklem1 26373 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ 𝐶 → 𝑁 ≤ (#‘(2nd ‘𝑊))) |
15 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) → 𝑁 ≤ (#‘(2nd ‘𝑊))) |
16 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) ∧ 𝑁 ∈ ℕ) → 𝑁 ≤ (#‘(2nd ‘𝑊))) |
17 | 10, 13, 16 | 3jca 1235 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊)))) |
18 | 8, 17 | jca 553 |
. . . . . . . . 9
⊢ (((𝑊 ∈ 𝐶 ∧ 𝑈 ∈ 𝐶) ∧ 𝑁 ∈ ℕ) → (((2nd
‘𝑈) ∈ Word 𝑉 ∧ (2nd
‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊))))) |
19 | 18 | exp31 628 |
. . . . . . . 8
⊢ (𝑊 ∈ 𝐶 → (𝑈 ∈ 𝐶 → (𝑁 ∈ ℕ → (((2nd
‘𝑈) ∈ Word 𝑉 ∧ (2nd
‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊))))))) |
20 | 19 | com13 86 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑈 ∈ 𝐶 → (𝑊 ∈ 𝐶 → (((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊))))))) |
21 | 20 | 3imp 1249 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → (((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊))))) |
22 | 21 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (((2nd
‘𝑈) ∈ Word 𝑉 ∧ (2nd
‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊))))) |
23 | 1, 2, 3, 4 | clwlkfclwwlk1hashn 26368 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝐶 → (#‘(1st
‘𝑈)) = 𝑁) |
24 | 23 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → (#‘(1st
‘𝑈)) = 𝑁) |
25 | 24 | opeq2d 4347 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → 〈0, (#‘(1st
‘𝑈))〉 = 〈0,
𝑁〉) |
26 | 25 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑈) substr 〈0, 𝑁〉)) |
27 | 1, 2, 3, 4 | clwlkfclwwlk1hashn 26368 |
. . . . . . . . . 10
⊢ (𝑊 ∈ 𝐶 → (#‘(1st
‘𝑊)) = 𝑁) |
28 | 27 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → (#‘(1st
‘𝑊)) = 𝑁) |
29 | 28 | opeq2d 4347 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → 〈0, (#‘(1st
‘𝑊))〉 = 〈0,
𝑁〉) |
30 | 29 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉) = ((2nd ‘𝑊) substr 〈0, 𝑁〉)) |
31 | 26, 30 | eqeq12d 2625 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → (((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉) ↔ ((2nd
‘𝑈) substr 〈0,
𝑁〉) = ((2nd
‘𝑊) substr 〈0,
𝑁〉))) |
32 | 31 | biimpa 500 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → ((2nd
‘𝑈) substr 〈0,
𝑁〉) = ((2nd
‘𝑊) substr 〈0,
𝑁〉)) |
33 | | simpl 472 |
. . . . . . 7
⊢
((((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊)))) →
((2nd ‘𝑈)
∈ Word 𝑉 ∧
(2nd ‘𝑊)
∈ Word 𝑉)) |
34 | | id 22 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
35 | 34, 34 | jca 553 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) |
36 | 35 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ≤
(#‘(2nd ‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd ‘𝑊))) → (𝑁 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
37 | 36 | adantl 481 |
. . . . . . 7
⊢
((((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊)))) → (𝑁 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) |
38 | | 3simpc 1053 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ≤
(#‘(2nd ‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd ‘𝑊))) → (𝑁 ≤ (#‘(2nd ‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd ‘𝑊)))) |
39 | 38 | adantl 481 |
. . . . . . 7
⊢
((((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊)))) → (𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊)))) |
40 | | swrdeq 13296 |
. . . . . . 7
⊢
((((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘(2nd ‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd ‘𝑊)))) → (((2nd
‘𝑈) substr 〈0,
𝑁〉) = ((2nd
‘𝑊) substr 〈0,
𝑁〉) ↔ (𝑁 = 𝑁 ∧ ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦)))) |
41 | 33, 37, 39, 40 | syl3anc 1318 |
. . . . . 6
⊢
((((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊)))) →
(((2nd ‘𝑈)
substr 〈0, 𝑁〉) =
((2nd ‘𝑊)
substr 〈0, 𝑁〉)
↔ (𝑁 = 𝑁 ∧ ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦)))) |
42 | | simpr 476 |
. . . . . 6
⊢ ((𝑁 = 𝑁 ∧ ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦)) |
43 | 41, 42 | syl6bi 242 |
. . . . 5
⊢
((((2nd ‘𝑈) ∈ Word 𝑉 ∧ (2nd ‘𝑊) ∈ Word 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑁 ≤ (#‘(2nd
‘𝑈)) ∧ 𝑁 ≤ (#‘(2nd
‘𝑊)))) →
(((2nd ‘𝑈)
substr 〈0, 𝑁〉) =
((2nd ‘𝑊)
substr 〈0, 𝑁〉)
→ ∀𝑦 ∈
(0..^𝑁)((2nd
‘𝑈)‘𝑦) = ((2nd
‘𝑊)‘𝑦))) |
44 | 22, 32, 43 | sylc 63 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦)) |
45 | | lbfzo0 12375 |
. . . . . . . . 9
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
46 | 45 | biimpri 217 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ∈
(0..^𝑁)) |
47 | 46 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → 0 ∈ (0..^𝑁)) |
48 | 47 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → 0 ∈ (0..^𝑁)) |
49 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 0 → ((2nd
‘𝑈)‘𝑦) = ((2nd
‘𝑈)‘0)) |
50 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 0 → ((2nd
‘𝑊)‘𝑦) = ((2nd
‘𝑊)‘0)) |
51 | 49, 50 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑦 = 0 → (((2nd
‘𝑈)‘𝑦) = ((2nd
‘𝑊)‘𝑦) ↔ ((2nd
‘𝑈)‘0) =
((2nd ‘𝑊)‘0))) |
52 | 51 | rspcv 3278 |
. . . . . 6
⊢ (0 ∈
(0..^𝑁) →
(∀𝑦 ∈
(0..^𝑁)((2nd
‘𝑈)‘𝑦) = ((2nd
‘𝑊)‘𝑦) → ((2nd
‘𝑈)‘0) =
((2nd ‘𝑊)‘0))) |
53 | 48, 52 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) → ((2nd ‘𝑈)‘0) = ((2nd
‘𝑊)‘0))) |
54 | 1, 2, 3, 4 | clwlkf1clwwlklem2 26374 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐶 → ((2nd ‘𝑈)‘0) = ((2nd
‘𝑈)‘𝑁)) |
55 | 54 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → ((2nd ‘𝑈)‘0) = ((2nd
‘𝑈)‘𝑁)) |
56 | 55 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → ((2nd
‘𝑈)‘0) =
((2nd ‘𝑈)‘𝑁)) |
57 | 1, 2, 3, 4 | clwlkf1clwwlklem2 26374 |
. . . . . . . 8
⊢ (𝑊 ∈ 𝐶 → ((2nd ‘𝑊)‘0) = ((2nd
‘𝑊)‘𝑁)) |
58 | 57 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → ((2nd ‘𝑊)‘0) = ((2nd
‘𝑊)‘𝑁)) |
59 | 58 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → ((2nd
‘𝑊)‘0) =
((2nd ‘𝑊)‘𝑁)) |
60 | 56, 59 | eqeq12d 2625 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (((2nd
‘𝑈)‘0) =
((2nd ‘𝑊)‘0) ↔ ((2nd
‘𝑈)‘𝑁) = ((2nd
‘𝑊)‘𝑁))) |
61 | 53, 60 | sylibd 228 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) → ((2nd ‘𝑈)‘𝑁) = ((2nd ‘𝑊)‘𝑁))) |
62 | 44, 61 | jcai 557 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ∧ ((2nd ‘𝑈)‘𝑁) = ((2nd ‘𝑊)‘𝑁))) |
63 | | elnn0uz 11601 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
64 | 9, 63 | sylib 207 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘0)) |
65 | 64 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → 𝑁 ∈
(ℤ≥‘0)) |
66 | 65 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → 𝑁 ∈
(ℤ≥‘0)) |
67 | | fzisfzounsn 12445 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...𝑁) = ((0..^𝑁) ∪ {𝑁})) |
68 | 66, 67 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (0...𝑁) = ((0..^𝑁) ∪ {𝑁})) |
69 | 68 | raleqdv 3121 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (∀𝑦 ∈ (0...𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ↔ ∀𝑦 ∈ ((0..^𝑁) ∪ {𝑁})((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦))) |
70 | | simpl1 1057 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → 𝑁 ∈ ℕ) |
71 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → ((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑈)‘𝑁)) |
72 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → ((2nd ‘𝑊)‘𝑦) = ((2nd ‘𝑊)‘𝑁)) |
73 | 71, 72 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑦 = 𝑁 → (((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ↔ ((2nd ‘𝑈)‘𝑁) = ((2nd ‘𝑊)‘𝑁))) |
74 | 73 | ralunsn 4360 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(∀𝑦 ∈
((0..^𝑁) ∪ {𝑁})((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ↔ (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ∧ ((2nd ‘𝑈)‘𝑁) = ((2nd ‘𝑊)‘𝑁)))) |
75 | 70, 74 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (∀𝑦 ∈ ((0..^𝑁) ∪ {𝑁})((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ↔ (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ∧ ((2nd ‘𝑈)‘𝑁) = ((2nd ‘𝑊)‘𝑁)))) |
76 | 69, 75 | bitrd 267 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → (∀𝑦 ∈ (0...𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ↔ (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦) ∧ ((2nd ‘𝑈)‘𝑁) = ((2nd ‘𝑊)‘𝑁)))) |
77 | 62, 76 | mpbird 246 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) ∧ ((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉)) → ∀𝑦 ∈ (0...𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦)) |
78 | 77 | ex 449 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → (((2nd ‘𝑈) substr 〈0,
(#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0,
(#‘(1st ‘𝑊))〉) → ∀𝑦 ∈ (0...𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦))) |