Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β π β π) |
2 | | extwwlkfab.v |
. . . . . 6
β’ π = (VtxβπΊ) |
3 | 2 | nbgrisvtx 28331 |
. . . . 5
β’ (π β (πΊ NeighbVtx π) β π β π) |
4 | 3 | ad2antll 728 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β π β π) |
5 | | simpl3 1194 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β π β
(β€β₯β3)) |
6 | | nbgrsym 28353 |
. . . . . . . 8
β’ (π β (πΊ NeighbVtx π) β π β (πΊ NeighbVtx π)) |
7 | | eqid 2737 |
. . . . . . . . . 10
β’
(EdgβπΊ) =
(EdgβπΊ) |
8 | 7 | nbusgreledg 28343 |
. . . . . . . . 9
β’ (πΊ β USGraph β (π β (πΊ NeighbVtx π) β {π, π} β (EdgβπΊ))) |
9 | 8 | biimpd 228 |
. . . . . . . 8
β’ (πΊ β USGraph β (π β (πΊ NeighbVtx π) β {π, π} β (EdgβπΊ))) |
10 | 6, 9 | biimtrid 241 |
. . . . . . 7
β’ (πΊ β USGraph β (π β (πΊ NeighbVtx π) β {π, π} β (EdgβπΊ))) |
11 | 10 | adantld 492 |
. . . . . 6
β’ (πΊ β USGraph β ((π β πΉ β§ π β (πΊ NeighbVtx π)) β {π, π} β (EdgβπΊ))) |
12 | 11 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π β πΉ β§ π β (πΊ NeighbVtx π)) β {π, π} β (EdgβπΊ))) |
13 | 12 | imp 408 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β {π, π} β (EdgβπΊ)) |
14 | | simprl 770 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β π β πΉ) |
15 | | extwwlkfab.f |
. . . . 5
β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) |
16 | 14, 15 | eleqtrdi 2848 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β π β (π(ClWWalksNOnβπΊ)(π β 2))) |
17 | 2, 7 | clwwlknonex2 29095 |
. . . 4
β’ (((π β π β§ π β π β§ π β (β€β₯β3))
β§ {π, π} β (EdgβπΊ) β§ π β (π(ClWWalksNOnβπΊ)(π β 2))) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ)) |
18 | 1, 4, 5, 13, 16, 17 | syl311anc 1385 |
. . 3
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ)) |
19 | 15 | eleq2i 2830 |
. . . . . . . 8
β’ (π β πΉ β π β (π(ClWWalksNOnβπΊ)(π β 2))) |
20 | | uz3m2nn 12823 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β3) β (π β 2) β β) |
21 | 20 | nnne0d 12210 |
. . . . . . . . . 10
β’ (π β
(β€β₯β3) β (π β 2) β 0) |
22 | 2, 7 | clwwlknonel 29081 |
. . . . . . . . . 10
β’ ((π β 2) β 0 β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
β’ (π β
(β€β₯β3) β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
24 | 23 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
25 | 19, 24 | bitrid 283 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β πΉ β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
26 | | 3simpa 1149 |
. . . . . . . . . . . . . 14
β’ ((π β Word π β§ (β―βπ) = (π β 2) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β (π β Word π β§ (β―βπ) = (π β 2))) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ (β―βπ) = (π β 2) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β§ π β (πΊ NeighbVtx π)) β (π β Word π β§ (β―βπ) = (π β 2))) |
28 | | simp32 1211 |
. . . . . . . . . . . . . 14
β’ ((π β Word π β§ (β―βπ) = (π β 2) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β π β π) |
29 | 28, 3 | anim12i 614 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ (β―βπ) = (π β 2) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β§ π β (πΊ NeighbVtx π)) β (π β π β§ π β π)) |
30 | | simpl33 1257 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ (β―βπ) = (π β 2) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β§ π β (πΊ NeighbVtx π)) β π β
(β€β₯β3)) |
31 | 27, 29, 30 | 3jca 1129 |
. . . . . . . . . . . 12
β’ (((π β Word π β§ (β―βπ) = (π β 2) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β§ π β (πΊ NeighbVtx π)) β ((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β
(β€β₯β3))) |
32 | 31 | 3exp1 1353 |
. . . . . . . . . . 11
β’ (π β Word π β ((β―βπ) = (π β 2) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β (πΊ NeighbVtx π) β ((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β
(β€β₯β3)))))) |
33 | 32 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β ((β―βπ) = (π β 2) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β (πΊ NeighbVtx π) β ((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β
(β€β₯β3)))))) |
34 | 33 | imp 408 |
. . . . . . . . 9
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2)) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β (πΊ NeighbVtx π) β ((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β
(β€β₯β3))))) |
35 | 34 | 3adant3 1133 |
. . . . . . . 8
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β (πΊ NeighbVtx π) β ((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β
(β€β₯β3))))) |
36 | 35 | com12 32 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (((π β Word
π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β (π β (πΊ NeighbVtx π) β ((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β
(β€β₯β3))))) |
37 | 25, 36 | sylbid 239 |
. . . . . 6
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β πΉ β (π β (πΊ NeighbVtx π) β ((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β
(β€β₯β3))))) |
38 | 37 | imp32 420 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β
(β€β₯β3))) |
39 | | numclwwlk1lem2foalem 29337 |
. . . . 5
β’ (((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β (β€β₯β3))
β ((((π ++
β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) = π β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) = π β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π)) |
40 | 38, 39 | syl 17 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) = π β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) = π β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π)) |
41 | | eleq1a 2833 |
. . . . . 6
β’ (π β πΉ β ((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) = π β (((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) β πΉ)) |
42 | 14, 41 | syl 17 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) = π β (((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) β πΉ)) |
43 | | eleq1a 2833 |
. . . . . 6
β’ (π β (πΊ NeighbVtx π) β ((((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) = π β (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) β (πΊ NeighbVtx π))) |
44 | 43 | ad2antll 728 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) = π β (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) β (πΊ NeighbVtx π))) |
45 | | idd 24 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π β (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π)) |
46 | 42, 44, 45 | 3anim123d 1444 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β (((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) = π β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) = π β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) β πΉ β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) β (πΊ NeighbVtx π) β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π))) |
47 | 40, 46 | mpd 15 |
. . 3
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) β πΉ β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) β (πΊ NeighbVtx π) β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π)) |
48 | | extwwlkfab.c |
. . . . 5
β’ πΆ = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) |
49 | 2, 48, 15 | extwwlkfabel 29339 |
. . . 4
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (((π ++
β¨βπββ©) ++ β¨βπββ©) β (ππΆπ) β (((π ++ β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ) β§ ((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) β πΉ β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) β (πΊ NeighbVtx π) β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π)))) |
50 | 49 | adantr 482 |
. . 3
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β (((π ++ β¨βπββ©) ++ β¨βπββ©) β (ππΆπ) β (((π ++ β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ) β§ ((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) β πΉ β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) β (πΊ NeighbVtx π) β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π)))) |
51 | 18, 47, 50 | mpbir2and 712 |
. 2
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (ππΆπ)) |
52 | 51 | ex 414 |
1
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π β πΉ β§ π β (πΊ NeighbVtx π)) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (ππΆπ))) |