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
β’ π = (π’ β (ππΆπ) β¦ β¨(π’ prefix (π β 2)), (π’β(π β 1))β©) |
5 | 1, 2, 3, 4 | numclwwlk1lem2f 29341 |
. 2
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β π:(ππΆπ)βΆ(πΉ Γ (πΊ NeighbVtx π))) |
6 | 1, 2, 3, 4 | numclwwlk1lem2fv 29342 |
. . . . . 6
β’ (π β (ππΆπ) β (πβπ) = β¨(π prefix (π β 2)), (πβ(π β 1))β©) |
7 | 6 | ad2antrl 727 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β (ππΆπ) β§ π β (ππΆπ))) β (πβπ) = β¨(π prefix (π β 2)), (πβ(π β 1))β©) |
8 | 1, 2, 3, 4 | numclwwlk1lem2fv 29342 |
. . . . . 6
β’ (π β (ππΆπ) β (πβπ) = β¨(π prefix (π β 2)), (πβ(π β 1))β©) |
9 | 8 | ad2antll 728 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β (ππΆπ) β§ π β (ππΆπ))) β (πβπ) = β¨(π prefix (π β 2)), (πβ(π β 1))β©) |
10 | 7, 9 | eqeq12d 2753 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β (ππΆπ) β§ π β (ππΆπ))) β ((πβπ) = (πβπ) β β¨(π prefix (π β 2)), (πβ(π β 1))β© = β¨(π prefix (π β 2)), (πβ(π β 1))β©)) |
11 | | ovex 7395 |
. . . . . 6
β’ (π prefix (π β 2)) β V |
12 | | fvex 6860 |
. . . . . 6
β’ (πβ(π β 1)) β V |
13 | 11, 12 | opth 5438 |
. . . . 5
β’
(β¨(π prefix
(π β 2)), (πβ(π β 1))β© = β¨(π prefix (π β 2)), (πβ(π β 1))β© β ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) |
14 | | uzuzle23 12821 |
. . . . . . . . 9
β’ (π β
(β€β₯β3) β π β
(β€β₯β2)) |
15 | 2 | 2clwwlkel 29335 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯β2))
β (π β (ππΆπ) β (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π))) |
16 | | isclwwlknon 29077 |
. . . . . . . . . . . 12
β’ (π β (π(ClWWalksNOnβπΊ)π) β (π β (π ClWWalksN πΊ) β§ (πβ0) = π)) |
17 | 16 | anbi1i 625 |
. . . . . . . . . . 11
β’ ((π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π) β ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) |
18 | 15, 17 | bitrdi 287 |
. . . . . . . . . 10
β’ ((π β π β§ π β (β€β₯β2))
β (π β (ππΆπ) β ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π))) |
19 | 2 | 2clwwlkel 29335 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯β2))
β (π β (ππΆπ) β (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π))) |
20 | | isclwwlknon 29077 |
. . . . . . . . . . . 12
β’ (π β (π(ClWWalksNOnβπΊ)π) β (π β (π ClWWalksN πΊ) β§ (πβ0) = π)) |
21 | 20 | anbi1i 625 |
. . . . . . . . . . 11
β’ ((π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π) β ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) |
22 | 19, 21 | bitrdi 287 |
. . . . . . . . . 10
β’ ((π β π β§ π β (β€β₯β2))
β (π β (ππΆπ) β ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π))) |
23 | 18, 22 | anbi12d 632 |
. . . . . . . . 9
β’ ((π β π β§ π β (β€β₯β2))
β ((π β (ππΆπ) β§ π β (ππΆπ)) β (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)))) |
24 | 14, 23 | sylan2 594 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯β3))
β ((π β (ππΆπ) β§ π β (ππΆπ)) β (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)))) |
25 | 24 | 3adant1 1131 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π β (ππΆπ) β§ π β (ππΆπ)) β (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)))) |
26 | 1 | clwwlknbp 29021 |
. . . . . . . . . . . . . . 15
β’ (π β (π ClWWalksN πΊ) β (π β Word π β§ (β―βπ) = π)) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β (π β Word π β§ (β―βπ) = π)) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (π β Word π β§ (β―βπ) = π)) |
29 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β (πβ0) = π) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (πβ0) = π) |
31 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (πβ(π β 2)) = π) |
32 | 29 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β π = (πβ0)) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β π = (πβ0)) |
34 | 31, 33 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (πβ(π β 2)) = (πβ0)) |
35 | 28, 30, 34 | jca32 517 |
. . . . . . . . . . . 12
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β ((π β Word π β§ (β―βπ) = π) β§ ((πβ0) = π β§ (πβ(π β 2)) = (πβ0)))) |
36 | 1 | clwwlknbp 29021 |
. . . . . . . . . . . . . . 15
β’ (π β (π ClWWalksN πΊ) β (π β Word π β§ (β―βπ) = π)) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β (π β Word π β§ (β―βπ) = π)) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (π β Word π β§ (β―βπ) = π)) |
39 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β (πβ0) = π) |
40 | 39 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (πβ0) = π) |
41 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (πβ(π β 2)) = π) |
42 | 39 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β π = (πβ0)) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β π = (πβ0)) |
44 | 41, 43 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (πβ(π β 2)) = (πβ0)) |
45 | 38, 40, 44 | jca32 517 |
. . . . . . . . . . . 12
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β ((π β Word π β§ (β―βπ) = π) β§ ((πβ0) = π β§ (πβ(π β 2)) = (πβ0)))) |
46 | | eqtr3 2763 |
. . . . . . . . . . . . . . . . 17
β’
(((β―βπ)
= π β§
(β―βπ) = π) β (β―βπ) = (β―βπ)) |
47 | 46 | expcom 415 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ) =
π β
((β―βπ) = π β (β―βπ) = (β―βπ))) |
48 | 47 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ (β―βπ) = π) β§ ((πβ0) = π β§ (πβ(π β 2)) = (πβ0))) β ((β―βπ) = π β (β―βπ) = (β―βπ))) |
49 | 48 | com12 32 |
. . . . . . . . . . . . . 14
β’
((β―βπ) =
π β (((π β Word π β§ (β―βπ) = π) β§ ((πβ0) = π β§ (πβ(π β 2)) = (πβ0))) β (β―βπ) = (β―βπ))) |
50 | 49 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ (β―βπ) = π) β§ ((πβ0) = π β§ (πβ(π β 2)) = (πβ0))) β (((π β Word π β§ (β―βπ) = π) β§ ((πβ0) = π β§ (πβ(π β 2)) = (πβ0))) β (β―βπ) = (β―βπ))) |
51 | 50 | imp 408 |
. . . . . . . . . . . 12
β’ ((((π β Word π β§ (β―βπ) = π) β§ ((πβ0) = π β§ (πβ(π β 2)) = (πβ0))) β§ ((π β Word π β§ (β―βπ) = π) β§ ((πβ0) = π β§ (πβ(π β 2)) = (πβ0)))) β (β―βπ) = (β―βπ)) |
52 | 35, 45, 51 | syl2an 597 |
. . . . . . . . . . 11
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (β―βπ) = (β―βπ)) |
53 | 52 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β3) β§ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β (β―βπ) = (β―βπ)) |
54 | 27 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β (β―βπ) = π) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (β―βπ) = π) |
56 | 55 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β π = (β―βπ)) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β π = (β―βπ)) |
58 | 57 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (π β 2) = ((β―βπ) β 2)) |
59 | 58 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (π prefix (π β 2)) = (π prefix ((β―βπ) β 2))) |
60 | 58 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (π prefix (π β 2)) = (π prefix ((β―βπ) β 2))) |
61 | 59, 60 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β ((π prefix (π β 2)) = (π prefix (π β 2)) β (π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)))) |
62 | 61 | biimpcd 249 |
. . . . . . . . . . . . . 14
β’ ((π prefix (π β 2)) = (π prefix (π β 2)) β ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)))) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1))) β ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)))) |
64 | 63 | impcom 409 |
. . . . . . . . . . . 12
β’
(((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β (π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2))) |
65 | 55 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β ((β―βπ) β 2) = (π β 2)) |
66 | 65 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (πβ((β―βπ) β 2)) = (πβ(π β 2))) |
67 | 66, 31 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β (πβ((β―βπ) β 2)) = π) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (πβ((β―βπ) β 2)) = π) |
69 | 41 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
β’ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β π = (πβ(π β 2))) |
70 | 69 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β π = (πβ(π β 2))) |
71 | 58 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (πβ(π β 2)) = (πβ((β―βπ) β 2))) |
72 | 70, 71 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β π = (πβ((β―βπ) β 2))) |
73 | 68, 72 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2))) |
74 | 73 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2))) |
75 | | lsw 14459 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
76 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπ) =
π β (πβ((β―βπ) β 1)) = (πβ(π β 1))) |
77 | 75, 76 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word π β§ (β―βπ) = π) β (lastSβπ) = (πβ(π β 1))) |
78 | 26, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π ClWWalksN πΊ) β (lastSβπ) = (πβ(π β 1))) |
79 | 78 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π ClWWalksN πΊ) β (πβ(π β 1)) = (lastSβπ)) |
80 | 79 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (πβ(π β 1)) = (lastSβπ)) |
81 | | lsw 14459 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
82 | 81 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Word π β§ (β―βπ) = π) β (lastSβπ) = (πβ((β―βπ) β 1))) |
83 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (β―βπ) β (π β 1) = ((β―βπ) β 1)) |
84 | 83 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ) =
π β (π β 1) = ((β―βπ) β 1)) |
85 | 84 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ) =
π β (πβ(π β 1)) = (πβ((β―βπ) β 1))) |
86 | 85 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ) =
π β
((lastSβπ) = (πβ(π β 1)) β (lastSβπ) = (πβ((β―βπ) β 1)))) |
87 | 86 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Word π β§ (β―βπ) = π) β ((lastSβπ) = (πβ(π β 1)) β (lastSβπ) = (πβ((β―βπ) β 1)))) |
88 | 82, 87 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Word π β§ (β―βπ) = π) β (lastSβπ) = (πβ(π β 1))) |
89 | 36, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π ClWWalksN πΊ) β (lastSβπ) = (πβ(π β 1))) |
90 | 89 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π ClWWalksN πΊ) β (πβ(π β 1)) = (lastSβπ)) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β (πβ(π β 1)) = (lastSβπ)) |
92 | 91 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (πβ(π β 1)) = (lastSβπ)) |
93 | 80, 92 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β ((πβ(π β 1)) = (πβ(π β 1)) β (lastSβπ) = (lastSβπ))) |
94 | 93 | biimpd 228 |
. . . . . . . . . . . . . 14
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β ((πβ(π β 1)) = (πβ(π β 1)) β (lastSβπ) = (lastSβπ))) |
95 | 94 | adantld 492 |
. . . . . . . . . . . . 13
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1))) β (lastSβπ) = (lastSβπ))) |
96 | 95 | imp 408 |
. . . . . . . . . . . 12
β’
(((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β (lastSβπ) = (lastSβπ)) |
97 | 64, 74, 96 | 3jca 1129 |
. . . . . . . . . . 11
β’
(((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ))) |
98 | 97 | 3adant1 1131 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β3) β§ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ))) |
99 | 1 | clwwlknwrd 29020 |
. . . . . . . . . . . . 13
β’ (π β (π ClWWalksN πΊ) β π β Word π) |
100 | 99 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β π β Word π) |
101 | 100 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β3) β§ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β π β Word π) |
102 | 1 | clwwlknwrd 29020 |
. . . . . . . . . . . . . 14
β’ (π β (π ClWWalksN πΊ) β π β Word π) |
103 | 102 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β π β Word π) |
104 | 103 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β π β Word π) |
105 | 104 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β3) β§ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β π β Word π) |
106 | | clwwlknlen 29018 |
. . . . . . . . . . . . . . 15
β’ (π β (π ClWWalksN πΊ) β (β―βπ) = π) |
107 | | eluz2b1 12851 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β2) β (π β β€ β§ 1 < π)) |
108 | | breq2 5114 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (β―βπ) β (1 < π β 1 <
(β―βπ))) |
109 | 108 | eqcoms 2745 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
π β (1 < π β 1 <
(β―βπ))) |
110 | 109 | biimpcd 249 |
. . . . . . . . . . . . . . . 16
β’ (1 <
π β
((β―βπ) = π β 1 <
(β―βπ))) |
111 | 107, 110 | simplbiim 506 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β2) β ((β―βπ) = π β 1 < (β―βπ))) |
112 | 14, 106, 111 | syl2imc 41 |
. . . . . . . . . . . . . 14
β’ (π β (π ClWWalksN πΊ) β (π β (β€β₯β3)
β 1 < (β―βπ))) |
113 | 112 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (π β (β€β₯β3)
β 1 < (β―βπ))) |
114 | 113 | impcom 409 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β3) β§ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π))) β 1 < (β―βπ)) |
115 | 114 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β3) β§ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β 1 <
(β―βπ)) |
116 | | 2swrd2eqwrdeq 14849 |
. . . . . . . . . . 11
β’ ((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ))))) |
117 | 101, 105,
115, 116 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β3) β§ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ))))) |
118 | 53, 98, 117 | mpbir2and 712 |
. . . . . . . . 9
β’ ((π β
(β€β₯β3) β§ (((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β§ ((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1)))) β π = π) |
119 | 118 | 3exp 1120 |
. . . . . . . 8
β’ (π β
(β€β₯β3) β ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1))) β π = π))) |
120 | 119 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π) β§ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β§ (πβ(π β 2)) = π)) β (((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1))) β π = π))) |
121 | 25, 120 | sylbid 239 |
. . . . . 6
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π β (ππΆπ) β§ π β (ππΆπ)) β (((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1))) β π = π))) |
122 | 121 | imp 408 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β (ππΆπ) β§ π β (ππΆπ))) β (((π prefix (π β 2)) = (π prefix (π β 2)) β§ (πβ(π β 1)) = (πβ(π β 1))) β π = π)) |
123 | 13, 122 | biimtrid 241 |
. . . 4
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β (ππΆπ) β§ π β (ππΆπ))) β (β¨(π prefix (π β 2)), (πβ(π β 1))β© = β¨(π prefix (π β 2)), (πβ(π β 1))β© β π = π)) |
124 | 10, 123 | sylbid 239 |
. . 3
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ (π β (ππΆπ) β§ π β (ππΆπ))) β ((πβπ) = (πβπ) β π = π)) |
125 | 124 | ralrimivva 3198 |
. 2
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β βπ β
(ππΆπ)βπ β (ππΆπ)((πβπ) = (πβπ) β π = π)) |
126 | | dff13 7207 |
. 2
β’ (π:(ππΆπ)β1-1β(πΉ Γ (πΊ NeighbVtx π)) β (π:(ππΆπ)βΆ(πΉ Γ (πΊ NeighbVtx π)) β§ βπ β (ππΆπ)βπ β (ππΆπ)((πβπ) = (πβπ) β π = π))) |
127 | 5, 125, 126 | sylanbrc 584 |
1
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β π:(ππΆπ)β1-1β(πΉ Γ (πΊ NeighbVtx π))) |