Proof of Theorem av-clwwlkextfrlem1
Step | Hyp | Ref
| Expression |
1 | | wwlknbp2 41063 |
. . . 4
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) |
2 | | simpll 786 |
. . . . . . 7
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (( lastS ‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)))) → 𝑊 ∈ Word (Vtx‘𝐺)) |
3 | | s1cl 13235 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (Vtx‘𝐺) → 〈“𝑍”〉 ∈ Word
(Vtx‘𝐺)) |
4 | 3 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑍 ∈
(Vtx‘𝐺)) →
〈“𝑍”〉
∈ Word (Vtx‘𝐺)) |
5 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((( lastS
‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0
∧ 𝑍 ∈
(Vtx‘𝐺))) →
〈“𝑍”〉
∈ Word (Vtx‘𝐺)) |
6 | 5 | adantl 481 |
. . . . . . 7
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (( lastS ‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)))) → 〈“𝑍”〉 ∈ Word
(Vtx‘𝐺)) |
7 | | nn0p1gt0 11199 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
1)) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑍 ∈
(Vtx‘𝐺)) → 0
< (𝑁 +
1)) |
9 | 8 | adantl 481 |
. . . . . . . . 9
⊢ ((( lastS
‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0
∧ 𝑍 ∈
(Vtx‘𝐺))) → 0
< (𝑁 +
1)) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (( lastS ‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)))) → 0 < (𝑁 + 1)) |
11 | | breq2 4587 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(𝑁 + 1) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
12 | 11 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → (0 < (#‘𝑊) ↔ 0 < (𝑁 + 1))) |
13 | 12 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (( lastS ‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)))) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
14 | 10, 13 | mpbird 246 |
. . . . . . 7
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (( lastS ‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)))) → 0 <
(#‘𝑊)) |
15 | | ccatfv0 13220 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 〈“𝑍”〉 ∈ Word
(Vtx‘𝐺) ∧ 0 <
(#‘𝑊)) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
16 | 2, 6, 14, 15 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (( lastS ‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)))) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
17 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) − 1) = ((𝑁 + 1) − 1)) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → ((#‘𝑊) − 1) = ((𝑁 + 1) −
1)) |
20 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
21 | | pncan1 10333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑍 ∈
(Vtx‘𝐺)) →
((𝑁 + 1) − 1) = 𝑁) |
24 | 23 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → ((𝑁 + 1) − 1) = 𝑁) |
25 | 19, 24 | eqtr2d 2645 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → 𝑁 = ((#‘𝑊) − 1)) |
26 | 25 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) = ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1))) |
27 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → 𝑊 ∈ Word (Vtx‘𝐺)) |
28 | 4 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → 〈“𝑍”〉 ∈ Word
(Vtx‘𝐺)) |
29 | 8 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → 0 < (𝑁 + 1)) |
30 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
31 | 29, 30 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → 0 < (#‘𝑊)) |
32 | | hashneq0 13016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅)) |
33 | 32 | bicomd 212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 ≠ ∅ ↔ 0 < (#‘𝑊))) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑊 ≠ ∅ ↔ 0 < (#‘𝑊))) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → (𝑊 ≠ ∅ ↔ 0 < (#‘𝑊))) |
36 | 31, 35 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → 𝑊 ≠ ∅) |
37 | | ccatval1lsw 13221 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 〈“𝑍”〉 ∈ Word
(Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
38 | 27, 28, 36, 37 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
39 | 26, 38 | eqtr2d 2645 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → ( lastS ‘𝑊) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) |
40 | 39 | neeq1d 2841 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → (( lastS ‘𝑊) ≠ (𝑊‘0) ↔ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0))) |
41 | 40 | biimpd 218 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺))) → (( lastS ‘𝑊) ≠ (𝑊‘0) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0))) |
42 | 41 | ex 449 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)) → (( lastS ‘𝑊) ≠ (𝑊‘0) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0)))) |
43 | 42 | com23 84 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → (( lastS ‘𝑊) ≠ (𝑊‘0) → ((𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0)))) |
44 | 43 | imp32 448 |
. . . . . 6
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (( lastS ‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)))) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0)) |
45 | 16, 44 | jca 553 |
. . . . 5
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (( lastS ‘𝑊) ≠ (𝑊‘0) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)))) → (((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0))) |
46 | 45 | exp32 629 |
. . . 4
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → (( lastS ‘𝑊) ≠ (𝑊‘0) → ((𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)) → (((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0))))) |
47 | 1, 46 | syl 17 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (( lastS ‘𝑊) ≠ (𝑊‘0) → ((𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)) → (((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0))))) |
48 | 47 | imp 444 |
. 2
⊢ ((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ ( lastS ‘𝑊) ≠ (𝑊‘0)) → ((𝑁 ∈ ℕ0 ∧ 𝑍 ∈ (Vtx‘𝐺)) → (((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0)))) |
49 | 48 | impcom 445 |
1
⊢ (((𝑁 ∈ ℕ0
∧ 𝑍 ∈
(Vtx‘𝐺)) ∧ (𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ ( lastS ‘𝑊) ≠ (𝑊‘0))) → (((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑍”〉)‘𝑁) ≠ (𝑊‘0))) |