Step | Hyp | Ref
| Expression |
1 | | extwwlkfab.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | extwwlkfab.c |
. . 3
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) |
3 | | extwwlkfab.f |
. . 3
⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) |
4 | | numclwwlk.t |
. . 3
⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ 〈(𝑢 substr 〈0, (𝑁 − 2)〉), (𝑢‘(𝑁 − 1))〉) |
5 | 1, 2, 3, 4 | numclwlk1lem2f 27345 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋))) |
6 | 1, 2, 3, 4 | numclwlk1lem2fv 27346 |
. . . . . 6
⊢ (𝑝 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑝) = 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉) |
7 | 6 | ad2antrl 764 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇‘𝑝) = 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉) |
8 | 1, 2, 3, 4 | numclwlk1lem2fv 27346 |
. . . . . 6
⊢ (𝑎 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑎) = 〈(𝑎 substr 〈0, (𝑁 − 2)〉), (𝑎‘(𝑁 − 1))〉) |
9 | 8 | ad2antll 765 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇‘𝑎) = 〈(𝑎 substr 〈0, (𝑁 − 2)〉), (𝑎‘(𝑁 − 1))〉) |
10 | 7, 9 | eqeq12d 2666 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑎) ↔ 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉 = 〈(𝑎 substr 〈0, (𝑁 − 2)〉), (𝑎‘(𝑁 − 1))〉)) |
11 | | ovex 6718 |
. . . . . 6
⊢ (𝑝 substr 〈0, (𝑁 − 2)〉) ∈
V |
12 | | fvex 6239 |
. . . . . 6
⊢ (𝑝‘(𝑁 − 1)) ∈ V |
13 | 11, 12 | opth 4974 |
. . . . 5
⊢
(〈(𝑝 substr
〈0, (𝑁 −
2)〉), (𝑝‘(𝑁 − 1))〉 =
〈(𝑎 substr 〈0,
(𝑁 − 2)〉),
(𝑎‘(𝑁 − 1))〉 ↔ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) |
14 | | uzuzle23 11767 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
15 | 2 | 2clwwlkel 27337 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑝 ∈ (𝑋𝐶𝑁) ↔ (𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑝‘(𝑁 − 2)) = 𝑋))) |
16 | | isclwwlknon 27065 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋)) |
17 | 16 | anbi1i 731 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ↔ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋)) |
18 | 15, 17 | syl6bb 276 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑝 ∈ (𝑋𝐶𝑁) ↔ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋))) |
19 | 2 | 2clwwlkel 27337 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑎 ∈ (𝑋𝐶𝑁) ↔ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))) |
20 | | isclwwlknon 27065 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋)) |
21 | 20 | anbi1i 731 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) ↔ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) |
22 | 19, 21 | syl6bb 276 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑎 ∈ (𝑋𝐶𝑁) ↔ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))) |
23 | 18, 22 | anbi12d 747 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))) |
24 | 14, 23 | sylan2 490 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))) |
25 | 24 | 3adant1 1099 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))) |
26 | 1 | clwwlknbp 26997 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁)) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁)) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁)) |
29 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (𝑝‘0) = 𝑋) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘0) = 𝑋) |
31 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘(𝑁 − 2)) = 𝑋) |
32 | 29 | eqcomd 2657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → 𝑋 = (𝑝‘0)) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑝‘0)) |
34 | 31, 33 | eqtrd 2685 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘(𝑁 − 2)) = (𝑝‘0)) |
35 | 28, 30, 34 | jca32 557 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)))) |
36 | 1 | clwwlknbp 26997 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁)) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁)) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁)) |
39 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎‘0) = 𝑋) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘0) = 𝑋) |
41 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘(𝑁 − 2)) = 𝑋) |
42 | 39 | eqcomd 2657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → 𝑋 = (𝑎‘0)) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑎‘0)) |
44 | 41, 43 | eqtrd 2685 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘(𝑁 − 2)) = (𝑎‘0)) |
45 | 38, 40, 44 | jca32 557 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) |
46 | | eqtr3 2672 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑝) =
𝑁 ∧ (#‘𝑎) = 𝑁) → (#‘𝑝) = (#‘𝑎)) |
47 | 46 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑎) = 𝑁 → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑎))) |
48 | 47 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑎))) |
49 | 48 | com12 32 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑝) = 𝑁 → (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (#‘𝑝) = (#‘𝑎))) |
50 | 49 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (#‘𝑝) = (#‘𝑎))) |
51 | 50 | imp 444 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (#‘𝑝) = (#‘𝑎)) |
52 | 35, 45, 51 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (#‘𝑝) = (#‘𝑎)) |
53 | 52 | 3ad2ant2 1103 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (#‘𝑝) = (#‘𝑎)) |
54 | 27 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (#‘𝑝) = 𝑁) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (#‘𝑝) = 𝑁) |
56 | 55 | eqcomd 2657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → 𝑁 = (#‘𝑝)) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑁 = (#‘𝑝)) |
58 | 57 | oveq1d 6705 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑁 − 2) = ((#‘𝑝) − 2)) |
59 | 58 | opeq2d 4440 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 〈0, (𝑁 − 2)〉 = 〈0, ((#‘𝑝) −
2)〉) |
60 | 59 | oveq2d 6706 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑝 substr 〈0, ((#‘𝑝) − 2)〉)) |
61 | 59 | oveq2d 6706 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉)) |
62 | 60, 61 | eqeq12d 2666 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ↔ (𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) −
2)〉))) |
63 | 62 | biimpcd 239 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) →
((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉))) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉))) |
65 | 64 | impcom 445 |
. . . . . . . . . . . 12
⊢
(((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉)) |
66 | 55 | oveq1d 6705 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → ((#‘𝑝) − 2) = (𝑁 − 2)) |
67 | 66 | fveq2d 6233 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘((#‘𝑝) − 2)) = (𝑝‘(𝑁 − 2))) |
68 | 67, 31 | eqtrd 2685 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘((#‘𝑝) − 2)) = 𝑋) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘((#‘𝑝) − 2)) = 𝑋) |
70 | 41 | eqcomd 2657 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑎‘(𝑁 − 2))) |
71 | 70 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑎‘(𝑁 − 2))) |
72 | 58 | fveq2d 6233 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎‘(𝑁 − 2)) = (𝑎‘((#‘𝑝) − 2))) |
73 | 71, 72 | eqtrd 2685 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑎‘((#‘𝑝) − 2))) |
74 | 69, 73 | eqtrd 2685 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2))) |
75 | 74 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2))) |
76 | | lsw 13384 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ Word 𝑉 → ( lastS ‘𝑝) = (𝑝‘((#‘𝑝) − 1))) |
77 | | oveq1 6697 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) = 𝑁 → ((#‘𝑝) − 1) = (𝑁 − 1)) |
78 | 77 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 1)) = (𝑝‘(𝑁 − 1))) |
79 | 76, 78 | sylan9eq 2705 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1))) |
80 | 26, 79 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1))) |
81 | 80 | eqcomd 2657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝‘(𝑁 − 1)) = ( lastS ‘𝑝)) |
82 | 81 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘(𝑁 − 1)) = ( lastS ‘𝑝)) |
83 | | lsw 13384 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ Word 𝑉 → ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1))) |
84 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1))) |
85 | | oveq1 6697 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 = (#‘𝑎) → (𝑁 − 1) = ((#‘𝑎) − 1)) |
86 | 85 | eqcoms 2659 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑎) = 𝑁 → (𝑁 − 1) = ((#‘𝑎) − 1)) |
87 | 86 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑎) = 𝑁 → (𝑎‘(𝑁 − 1)) = (𝑎‘((#‘𝑎) − 1))) |
88 | 87 | eqeq2d 2661 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑎) = 𝑁 → (( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1)))) |
89 | 88 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → (( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1)))) |
90 | 84, 89 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → ( lastS ‘𝑎) = (𝑎‘(𝑁 − 1))) |
91 | 36, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → ( lastS ‘𝑎) = (𝑎‘(𝑁 − 1))) |
92 | 91 | eqcomd 2657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎)) |
93 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎)) |
94 | 93 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎)) |
95 | 82, 94 | eqeq12d 2666 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑝) = ( lastS ‘𝑎))) |
96 | 95 | biimpd 219 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)) → ( lastS ‘𝑝) = ( lastS ‘𝑎))) |
97 | 96 | adantld 482 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → ( lastS ‘𝑝) = ( lastS ‘𝑎))) |
98 | 97 | imp 444 |
. . . . . . . . . . . 12
⊢
(((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ( lastS ‘𝑝) = ( lastS ‘𝑎)) |
99 | 65, 75, 98 | 3jca 1261 |
. . . . . . . . . . 11
⊢
(((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎))) |
100 | 99 | 3adant1 1099 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎))) |
101 | 1 | clwwlknwrd 26996 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → 𝑝 ∈ Word 𝑉) |
102 | 101 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑝 ∈ Word 𝑉) |
103 | 102 | 3ad2ant2 1103 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑝 ∈ Word 𝑉) |
104 | 1 | clwwlknwrd 26996 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → 𝑎 ∈ Word 𝑉) |
105 | 104 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → 𝑎 ∈ Word 𝑉) |
106 | 105 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑎 ∈ Word 𝑉) |
107 | 106 | 3ad2ant2 1103 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑎 ∈ Word 𝑉) |
108 | | clwwlknlen 26994 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (#‘𝑝) = 𝑁) |
109 | | eluz2b1 11797 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁)) |
110 | | breq2 4689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (#‘𝑝) → (1 < 𝑁 ↔ 1 < (#‘𝑝))) |
111 | 110 | eqcoms 2659 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑝) = 𝑁 → (1 < 𝑁 ↔ 1 < (#‘𝑝))) |
112 | 111 | biimpcd 239 |
. . . . . . . . . . . . . . . . 17
⊢ (1 <
𝑁 → ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝))) |
113 | 109, 112 | simplbiim 659 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝))) |
114 | 14, 108, 113 | syl2imc 41 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑁 ∈ (ℤ≥‘3)
→ 1 < (#‘𝑝))) |
115 | 114 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑁 ∈ (ℤ≥‘3)
→ 1 < (#‘𝑝))) |
116 | 115 | impcom 445 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))) → 1 < (#‘𝑝)) |
117 | 116 | 3adant3 1101 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 1 < (#‘𝑝)) |
118 | 103, 107,
117 | 3jca 1261 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 ∈ Word 𝑉 ∧ 𝑎 ∈ Word 𝑉 ∧ 1 < (#‘𝑝))) |
119 | | 2swrd2eqwrdeq 13742 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ Word 𝑉 ∧ 𝑎 ∈ Word 𝑉 ∧ 1 < (#‘𝑝)) → (𝑝 = 𝑎 ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎))))) |
120 | 118, 119 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 = 𝑎 ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎))))) |
121 | 53, 100, 120 | mpbir2and 977 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑝 = 𝑎) |
122 | 121 | 3exp 1283 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎))) |
123 | 122 | 3ad2ant3 1104 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎))) |
124 | 25, 123 | sylbid 230 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎))) |
125 | 124 | imp 444 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)) |
126 | 13, 125 | syl5bi 232 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉 = 〈(𝑎 substr 〈0, (𝑁 − 2)〉), (𝑎‘(𝑁 − 1))〉 → 𝑝 = 𝑎)) |
127 | 10, 126 | sylbid 230 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎)) |
128 | 127 | ralrimivva 3000 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∀𝑝 ∈
(𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎)) |
129 | | dff13 6552 |
. 2
⊢ (𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)) ↔ (𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋)) ∧ ∀𝑝 ∈ (𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎))) |
130 | 5, 128, 129 | sylanbrc 699 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋))) |