Proof of Theorem clwwlkextfrlem1
Step | Hyp | Ref
| Expression |
1 | | wwlknimpb 26232 |
. . . 4
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) |
2 | | simprll 798 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → 𝑊 ∈ Word 𝑉) |
3 | | s1cl 13235 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ 𝑉 → 〈“𝑍”〉 ∈ Word 𝑉) |
4 | 3 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → 〈“𝑍”〉 ∈ Word 𝑉) |
5 | 4 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → 〈“𝑍”〉 ∈ Word 𝑉) |
6 | | nnnn0 11176 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
7 | | nn0p1gt0 11199 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
1)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 0 <
(𝑁 + 1)) |
9 | 8 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → 0 < (𝑁 + 1)) |
10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → 0 < (𝑁 + 1)) |
11 | | breq2 4587 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) =
(𝑁 + 1) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (0 < (#‘𝑊) ↔ 0 < (𝑁 + 1))) |
13 | 12 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → (0 < (#‘𝑊) ↔ 0 < (𝑁 + 1))) |
14 | 10, 13 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → 0 < (#‘𝑊)) |
15 | | ccatfv0 13220 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
16 | 2, 5, 14, 15 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
17 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → (𝑊‘0) = 𝑋) |
18 | 17 | adantl 481 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → (𝑊‘0) = 𝑋) |
19 | 16, 18 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → ((𝑊 ++ 〈“𝑍”〉)‘0) = 𝑋) |
20 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) − 1) = ((𝑁 + 1) − 1)) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → ((#‘𝑊) − 1) = ((𝑁 + 1) − 1)) |
23 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
24 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
26 | 25 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → ((𝑁 + 1) − 1) = 𝑁) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → ((𝑁 + 1) − 1) = 𝑁) |
28 | 22, 27 | eqtr2d 2645 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → 𝑁 = ((#‘𝑊) − 1)) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) = ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1))) |
30 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → 𝑊 ∈ Word 𝑉) |
31 | 4 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → 〈“𝑍”〉 ∈ Word 𝑉) |
32 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → 0 < (𝑁 + 1)) |
33 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → (0 < (#‘𝑊) ↔ 0 < (𝑁 + 1))) |
34 | 32, 33 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → 0 < (#‘𝑊)) |
35 | | hashneq0 13016 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅)) |
36 | 35 | ad2antrl 760 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅)) |
37 | 34, 36 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → 𝑊 ≠ ∅) |
38 | | ccatval1lsw 13221 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
39 | 30, 31, 37, 38 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
40 | 29, 39 | eqtr2d 2645 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → ( lastS ‘𝑊) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) |
41 | 40 | neeq1d 2841 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → (( lastS ‘𝑊) ≠ 𝑋 ↔ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋)) |
42 | 41 | biimpd 218 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → (( lastS ‘𝑊) ≠ 𝑋 → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋)) |
43 | 42 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (( lastS ‘𝑊) ≠ 𝑋 → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋))) |
44 | 43 | com13 86 |
. . . . . . . . . 10
⊢ (( lastS
‘𝑊) ≠ 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋))) |
45 | 44 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋))) |
46 | 45 | com13 86 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋))) |
47 | 46 | imp32 448 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋) |
48 | 19, 47 | jca 553 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → (((𝑊 ++ 〈“𝑍”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋)) |
49 | 48 | expcom 450 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → (((𝑊 ++ 〈“𝑍”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋))) |
50 | 49 | exp32 629 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑊‘0) = 𝑋 → (( lastS ‘𝑊) ≠ 𝑋 → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → (((𝑊 ++ 〈“𝑍”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋))))) |
51 | 1, 50 | syl 17 |
. . 3
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑊‘0) = 𝑋 → (( lastS ‘𝑊) ≠ 𝑋 → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → (((𝑊 ++ 〈“𝑍”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋))))) |
52 | 51 | 3imp 1249 |
. 2
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) → (((𝑊 ++ 〈“𝑍”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋))) |
53 | 52 | impcom 445 |
1
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑍 ∈ 𝑉) ∧ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → (((𝑊 ++ 〈“𝑍”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ 𝑋)) |