Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝐺 ∈ USGraph
) |
2 | | uz3m2nn 11607 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
3 | 2 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ) |
4 | | simp2 1055 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝑉) |
5 | | av-extwwlkfab.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
6 | | av-extwwlkfab.v |
. . . . . . . . . . 11
⊢ 𝑉 = (Vtx‘𝐺) |
7 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
8 | 5, 6, 7 | av-numclwwlkovfel2 41514 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ (𝑁 − 2) ∈ ℕ ∧
𝑋 ∈ 𝑉) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋))) |
9 | 1, 3, 4, 8 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋))) |
10 | 5, 6, 7 | av-numclwwlkovf2ex 41517 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺)) |
11 | 10 | ad4ant134 1288 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺)) |
12 | 6 | nbgrisvtx 40581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ USGraph ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄 ∈ 𝑉) |
13 | 12 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 ∈ 𝑉)) |
14 | 13 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 ∈ 𝑉)) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 ∈ 𝑉)) |
16 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑄 ∈ 𝑉) → 𝑃 ∈ Word 𝑉) |
17 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑋 ∈ 𝑉 → 〈“𝑋”〉 ∈ Word 𝑉) |
18 | 17 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈“𝑋”〉 ∈ Word 𝑉) |
19 | 18 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 〈“𝑋”〉 ∈ Word 𝑉) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑄 ∈ 𝑉) → 〈“𝑋”〉 ∈ Word 𝑉) |
21 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑄 ∈ 𝑉 → 〈“𝑄”〉 ∈ Word 𝑉) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑄 ∈ 𝑉) → 〈“𝑄”〉 ∈ Word 𝑉) |
23 | | ccatass 13224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑄”〉 ∈ Word 𝑉) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) = (𝑃 ++ (〈“𝑋”〉 ++
〈“𝑄”〉))) |
24 | 23 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑄”〉 ∈ Word 𝑉) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) =
((𝑃 ++ (〈“𝑋”〉 ++
〈“𝑄”〉)) substr 〈0, (𝑁 −
2)〉)) |
25 | 16, 20, 22, 24 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑄 ∈ 𝑉) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) =
((𝑃 ++ (〈“𝑋”〉 ++
〈“𝑄”〉)) substr 〈0, (𝑁 −
2)〉)) |
26 | | ccatcl 13212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑄”〉 ∈ Word 𝑉) → (〈“𝑋”〉 ++ 〈“𝑄”〉) ∈ Word 𝑉) |
27 | 19, 21, 26 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑄 ∈ 𝑉) → (〈“𝑋”〉 ++
〈“𝑄”〉) ∈ Word 𝑉) |
28 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) → (#‘𝑃) = (𝑁 − 2)) |
29 | 28 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) → (𝑁 − 2) = (#‘𝑃)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑁 − 2) =
(#‘𝑃)) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑄 ∈ 𝑉) → (𝑁 − 2) = (#‘𝑃)) |
32 | | swrdccatid 13348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ Word 𝑉 ∧ (〈“𝑋”〉 ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ (𝑁 − 2) = (#‘𝑃)) → ((𝑃 ++ (〈“𝑋”〉 ++ 〈“𝑄”〉)) substr 〈0,
(𝑁 − 2)〉) =
𝑃) |
33 | 16, 27, 31, 32 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑄 ∈ 𝑉) → ((𝑃 ++ (〈“𝑋”〉 ++ 〈“𝑄”〉)) substr 〈0,
(𝑁 − 2)〉) =
𝑃) |
34 | 25, 33 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑄 ∈ 𝑉) → 𝑃 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 −
2)〉)) |
35 | 34 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ 𝑉 → 𝑃 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 −
2)〉)))) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ 𝑉 → 𝑃 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 −
2)〉)))) |
37 | 36 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ 𝑉 → 𝑃 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 −
2)〉))) |
38 | 15, 37 | syld 46 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑃 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 −
2)〉))) |
39 | 38 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑃 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 −
2)〉)) |
40 | 39 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)))) |
41 | 40 | biimpd 218 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)))) |
42 | 41 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2))) |
43 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2))) |
44 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → 𝑋 ∈ 𝑉) |
45 | 44 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) |
46 | | ccatw2s1p2 13266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((𝑁 − 2) + 1)) = 𝑄) |
47 | 43, 45, 46 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((𝑁 − 2) + 1)) = 𝑄) |
48 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
49 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℂ) |
50 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℂ) |
51 | | subsub 10190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
52 | 51 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 2) + 1) = (𝑁 − (2 − 1))) |
53 | 48, 49, 50, 52 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) + 1) = (𝑁 − (2 − 1))) |
54 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (2
− 1) = 1 |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → (2 − 1) = 1) |
56 | 55 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (2 − 1)) = (𝑁 − 1)) |
57 | 53, 56 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
58 | 57 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑁 − 2) + 1)
= (𝑁 −
1)) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
61 | 60 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((𝑁 − 2) + 1)) = (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘(𝑁 − 1))) |
62 | 47, 61 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → 𝑄 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1))) |
63 | 62 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ 𝑉 → 𝑄 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)))) |
64 | 15, 63 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)))) |
65 | 64 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋))) → 𝑄 = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1))) |
66 | 65 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋))) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋))) |
67 | 66 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋))) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋))) |
68 | 67 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋)))) |
69 | 68 | pm2.43a 52 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋))) |
70 | 69 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋)) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋)) |
72 | | ccatw2s1p1 13265 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋) |
73 | 43, 45, 72 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋) |
74 | 73 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ 𝑉 → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)) |
75 | 15, 74 | syld 46 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)) |
76 | 75 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋) |
78 | 42, 71, 77 | 3jca 1235 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)) |
79 | 11, 78 | jca 553 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋))) |
80 | 79 | exp31 628 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋))))) |
81 | 80 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)))))) |
82 | 81 | exp31 628 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)))))))) |
83 | 82 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)))))))) |
84 | 83 | 3imp 1249 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)))))) |
85 | 84 | com12 32 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)))))) |
86 | 9, 85 | sylbid 229 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)))))) |
87 | 86 | com14 94 |
. . . . . . 7
⊢ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ++
〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)))))) |
88 | 87 | pm2.43i 50 |
. . . . . 6
⊢ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ++
〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋))))) |
89 | 88 | imp 444 |
. . . . 5
⊢ ((𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ++
〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)))) |
90 | 89 | impcom 445 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋))) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋))) |
91 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑤 = ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) → (𝑤 substr 〈0, (𝑁 − 2)〉) = (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉) substr 〈0, (𝑁 −
2)〉)) |
92 | 91 | eleq1d 2672 |
. . . . . 6
⊢ (𝑤 = ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ↔ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)))) |
93 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑤 = ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) → (𝑤‘(𝑁 − 1)) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1))) |
94 | 93 | eleq1d 2672 |
. . . . . 6
⊢ (𝑤 = ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) → ((𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ↔ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋))) |
95 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑤 = ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) → (𝑤‘(𝑁 − 2)) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2))) |
96 | 95 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑤 = ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) → ((𝑤‘(𝑁 − 2)) = 𝑋 ↔ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋)) |
97 | 92, 94, 96 | 3anbi123d 1391 |
. . . . 5
⊢ (𝑤 = ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋))) |
98 | 97 | elrab 3331 |
. . . 4
⊢ (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉) ∈ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)} ↔ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ∧ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑁 − 2)) = 𝑋))) |
99 | 90, 98 | sylibr 223 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋))) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
100 | | av-extwwlkfab.c |
. . . . 5
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
101 | 6, 5, 100 | av-extwwlkfab 41520 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
102 | 101 | adantr 480 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋))) → (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
103 | 99, 102 | eleqtrrd 2691 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋))) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑋𝐶𝑁)) |
104 | 103 | ex 449 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑋𝐶𝑁))) |