Step | Hyp | Ref
| Expression |
1 | | elwwlks2.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | 1 | wspthsnwspthsnon 28903 |
. . 3
β’ (π β (2 WSPathsN πΊ) β βπ β π βπ β π π β (π(2 WSPathsNOn πΊ)π)) |
3 | 2 | a1i 11 |
. 2
β’ (πΊ β UPGraph β (π β (2 WSPathsN πΊ) β βπ β π βπ β π π β (π(2 WSPathsNOn πΊ)π))) |
4 | 1 | elwspths2on 28947 |
. . . 4
β’ ((πΊ β UPGraph β§ π β π β§ π β π) β (π β (π(2 WSPathsNOn πΊ)π) β βπ β π (π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π)))) |
5 | 4 | 3expb 1121 |
. . 3
β’ ((πΊ β UPGraph β§ (π β π β§ π β π)) β (π β (π(2 WSPathsNOn πΊ)π) β βπ β π (π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π)))) |
6 | 5 | 2rexbidva 3208 |
. 2
β’ (πΊ β UPGraph β
(βπ β π βπ β π π β (π(2 WSPathsNOn πΊ)π) β βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π)))) |
7 | | rexcom 3272 |
. . . 4
β’
(βπ β
π βπ β π (π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π)) β βπ β π βπ β π (π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π))) |
8 | | wspthnon 28845 |
. . . . . . 7
β’
(β¨βπππββ© β (π(2 WSPathsNOn πΊ)π) β (β¨βπππββ© β (π(2 WWalksNOn πΊ)π) β§ βπ π(π(SPathsOnβπΊ)π)β¨βπππββ©)) |
9 | | ancom 462 |
. . . . . . . . 9
β’
((β¨βπππββ© β (π(2 WWalksNOn πΊ)π) β§ βπ π(π(SPathsOnβπΊ)π)β¨βπππββ©) β (βπ π(π(SPathsOnβπΊ)π)β¨βπππββ© β§ β¨βπππββ© β (π(2 WWalksNOn πΊ)π))) |
10 | | 19.41v 1954 |
. . . . . . . . 9
β’
(βπ(π(π(SPathsOnβπΊ)π)β¨βπππββ© β§ β¨βπππββ© β (π(2 WWalksNOn πΊ)π)) β (βπ π(π(SPathsOnβπΊ)π)β¨βπππββ© β§ β¨βπππββ© β (π(2 WWalksNOn πΊ)π))) |
11 | 9, 10 | bitr4i 278 |
. . . . . . . 8
β’
((β¨βπππββ© β (π(2 WWalksNOn πΊ)π) β§ βπ π(π(SPathsOnβπΊ)π)β¨βπππββ©) β βπ(π(π(SPathsOnβπΊ)π)β¨βπππββ© β§ β¨βπππββ© β (π(2 WWalksNOn πΊ)π))) |
12 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((πΊ β UPGraph β§ π β π) β π β π) |
13 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β π β π) |
14 | 12, 13 | anim12i 614 |
. . . . . . . . . . . . 13
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (π β π β§ π β π)) |
15 | | vex 3448 |
. . . . . . . . . . . . . 14
β’ π β V |
16 | | s3cli 14776 |
. . . . . . . . . . . . . 14
β’
β¨βπππββ© β Word V |
17 | 15, 16 | pm3.2i 472 |
. . . . . . . . . . . . 13
β’ (π β V β§
β¨βπππββ© β Word V) |
18 | 1 | isspthonpth 28739 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β π) β§ (π β V β§ β¨βπππββ© β Word V)) β (π(π(SPathsOnβπΊ)π)β¨βπππββ© β (π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π))) |
19 | 14, 17, 18 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (π(π(SPathsOnβπΊ)π)β¨βπππββ© β (π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π))) |
20 | | wwlknon 28844 |
. . . . . . . . . . . . 13
β’
(β¨βπππββ© β (π(2 WWalksNOn πΊ)π) β (β¨βπππββ© β (2 WWalksN πΊ) β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) |
21 | | 2nn0 12435 |
. . . . . . . . . . . . . . 15
β’ 2 β
β0 |
22 | | iswwlksn 28825 |
. . . . . . . . . . . . . . 15
β’ (2 β
β0 β (β¨βπππββ© β (2 WWalksN πΊ) β (β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)))) |
23 | 21, 22 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (β¨βπππββ© β (2 WWalksN πΊ) β (β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)))) |
24 | 23 | 3anbi1d 1441 |
. . . . . . . . . . . . 13
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β ((β¨βπππββ© β (2 WWalksN πΊ) β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π) β ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) |
25 | 20, 24 | bitrid 283 |
. . . . . . . . . . . 12
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (β¨βπππββ© β (π(2 WWalksNOn πΊ)π) β ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) |
26 | 19, 25 | anbi12d 632 |
. . . . . . . . . . 11
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β ((π(π(SPathsOnβπΊ)π)β¨βπππββ© β§ β¨βπππββ© β (π(2 WWalksNOn πΊ)π)) β ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)))) |
27 | 26 | adantr 482 |
. . . . . . . . . 10
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β ((π(π(SPathsOnβπΊ)π)β¨βπππββ© β§ β¨βπππββ© β (π(2 WWalksNOn πΊ)π)) β ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)))) |
28 | 16 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β β¨βπππββ© β Word V) |
29 | | simprl1 1219 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) β π(SPathsβπΊ)β¨βπππββ©) |
30 | | spthiswlk 28718 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(SPathsβπΊ)β¨βπππββ© β π(WalksβπΊ)β¨βπππββ©) |
31 | | wlklenvm1 28612 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(WalksβπΊ)β¨βπππββ© β (β―βπ) =
((β―ββ¨βπππββ©) β 1)) |
32 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
= ((β―ββ¨βπππββ©) β 1) β§
((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) β (β―βπ) = ((β―ββ¨βπππββ©) β 1)) |
33 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―ββ¨βπππββ©) = (2 + 1) β
((β―ββ¨βπππββ©) β 1) = ((2 + 1) β
1)) |
34 | | 2cn 12233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 2 β
β |
35 | | pncan1 11584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (2 β
β β ((2 + 1) β 1) = 2) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((2 + 1)
β 1) = 2 |
37 | 33, 36 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―ββ¨βπππββ©) = (2 + 1) β
((β―ββ¨βπππββ©) β 1) =
2) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β
((β―ββ¨βπππββ©) β 1) =
2) |
39 | 38 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π) β ((β―ββ¨βπππββ©) β 1) =
2) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
= ((β―ββ¨βπππββ©) β 1) β§
((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) β ((β―ββ¨βπππββ©) β 1) =
2) |
41 | 32, 40 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ)
= ((β―ββ¨βπππββ©) β 1) β§
((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) β (β―βπ) = 2) |
42 | 41 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπ) =
((β―ββ¨βπππββ©) β 1) β
(((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π) β (β―βπ) = 2)) |
43 | 30, 31, 42 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ (π(SPathsβπΊ)β¨βπππββ© β (((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π) β (β―βπ) = 2)) |
44 | 43 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β (((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π) β (β―βπ) = 2)) |
45 | 44 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’ (((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) β (β―βπ) = 2) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) β (β―βπ) = 2) |
47 | | s3fv0 14786 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β V β
(β¨βπππββ©β0) = π) |
48 | 47 | elv 3450 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨βπππββ©β0) = π |
49 | 48 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . 18
β’ π = (β¨βπππββ©β0) |
50 | | s3fv1 14787 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β V β
(β¨βπππββ©β1) = π) |
51 | 50 | elv 3450 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨βπππββ©β1) = π |
52 | 51 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . 18
β’ π = (β¨βπππββ©β1) |
53 | | s3fv2 14788 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β V β
(β¨βπππββ©β2) = π) |
54 | 53 | elv 3450 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨βπππββ©β2) = π |
55 | 54 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . 18
β’ π = (β¨βπππββ©β2) |
56 | 49, 52, 55 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . 17
β’ (π = (β¨βπππββ©β0) β§ π = (β¨βπππββ©β1) β§ π = (β¨βπππββ©β2)) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) β (π = (β¨βπππββ©β0) β§ π = (β¨βπππββ©β1) β§ π = (β¨βπππββ©β2))) |
58 | 29, 46, 57 | 3jca 1129 |
. . . . . . . . . . . . . . 15
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) β (π(SPathsβπΊ)β¨βπππββ© β§ (β―βπ) = 2 β§ (π = (β¨βπππββ©β0) β§ π = (β¨βπππββ©β1) β§ π = (β¨βπππββ©β2)))) |
59 | | breq2 5110 |
. . . . . . . . . . . . . . . . 17
β’ (π = β¨βπππββ© β (π(SPathsβπΊ)π β π(SPathsβπΊ)β¨βπππββ©)) |
60 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β¨βπππββ© β (πβ0) = (β¨βπππββ©β0)) |
61 | 60 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’ (π = β¨βπππββ© β (π = (πβ0) β π = (β¨βπππββ©β0))) |
62 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β¨βπππββ© β (πβ1) = (β¨βπππββ©β1)) |
63 | 62 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’ (π = β¨βπππββ© β (π = (πβ1) β π = (β¨βπππββ©β1))) |
64 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β¨βπππββ© β (πβ2) = (β¨βπππββ©β2)) |
65 | 64 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’ (π = β¨βπππββ© β (π = (πβ2) β π = (β¨βπππββ©β2))) |
66 | 61, 63, 65 | 3anbi123d 1437 |
. . . . . . . . . . . . . . . . 17
β’ (π = β¨βπππββ© β ((π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)) β (π = (β¨βπππββ©β0) β§ π = (β¨βπππββ©β1) β§ π = (β¨βπππββ©β2)))) |
67 | 59, 66 | 3anbi13d 1439 |
. . . . . . . . . . . . . . . 16
β’ (π = β¨βπππββ© β ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π(SPathsβπΊ)β¨βπππββ© β§ (β―βπ) = 2 β§ (π = (β¨βπππββ©β0) β§ π = (β¨βπππββ©β1) β§ π = (β¨βπππββ©β2))))) |
68 | 67 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) β ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π(SPathsβπΊ)β¨βπππββ© β§ (β―βπ) = 2 β§ (π = (β¨βπππββ©β0) β§ π = (β¨βπππββ©β1) β§ π = (β¨βπππββ©β2))))) |
69 | 58, 68 | mpbird 257 |
. . . . . . . . . . . . . 14
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) β (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) |
70 | 69 | ex 414 |
. . . . . . . . . . . . 13
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) β (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
71 | 28, 70 | spcimedv 3553 |
. . . . . . . . . . . 12
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) β βπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
72 | | spthiswlk 28718 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π(SPathsβπΊ)π β π(WalksβπΊ)π) |
73 | | wlklenvp1 28608 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π(WalksβπΊ)π β (β―βπ) = ((β―βπ) + 1)) |
74 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ) =
2 β ((β―βπ)
+ 1) = (2 + 1)) |
75 | | 2p1e3 12300 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (2 + 1) =
3 |
76 | 74, 75 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ) =
2 β ((β―βπ)
+ 1) = 3) |
77 | 76 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ) =
2 β ((β―βπ)
= ((β―βπ) + 1)
β (β―βπ) =
3)) |
78 | 77 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ) =
((β―βπ) + 1)
β ((β―βπ) =
2 β (β―βπ)
= 3)) |
79 | 72, 73, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(SPathsβπΊ)π β ((β―βπ) = 2 β (β―βπ) = 3)) |
80 | 79 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π(SPathsβπΊ)π β§ (β―βπ) = 2) β (β―βπ) = 3) |
81 | 80 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (β―βπ) = 3) |
82 | 81 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β (β―βπ) = 3) |
83 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ0) β (πβ0) = π) |
84 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ1) β (πβ1) = π) |
85 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ2) β (πβ2) = π) |
86 | 83, 84, 85 | 3anbi123i 1156 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)) β ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)) |
87 | 86 | biimpi 215 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)) β ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)) |
88 | 87 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)) |
89 | 88 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)) |
90 | 82, 89 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β ((β―βπ) = 3 β§ ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π))) |
91 | 1 | wlkpwrd 28607 |
. . . . . . . . . . . . . . . . . . 19
β’ (π(WalksβπΊ)π β π β Word π) |
92 | 72, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π(SPathsβπΊ)π β π β Word π) |
93 | 92 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
β’ ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β π β Word π) |
94 | 12 | anim1i 616 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (π β π β§ (π β π β§ π β π))) |
95 | | 3anass 1096 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ π β π β§ π β π) β (π β π β§ (π β π β§ π β π))) |
96 | 94, 95 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (π β π β§ π β π β§ π β π)) |
97 | | eqwrds3 14856 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word π β§ (π β π β§ π β π β§ π β π)) β (π = β¨βπππββ© β ((β―βπ) = 3 β§ ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)))) |
98 | 93, 96, 97 | syl2anr 598 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β (π = β¨βπππββ© β ((β―βπ) = 3 β§ ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)))) |
99 | 90, 98 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β π = β¨βπππββ©) |
100 | 59 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(SPathsβπΊ)π β (π = β¨βπππββ© β π(SPathsβπΊ)β¨βπππββ©)) |
101 | 100 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π = β¨βπππββ© β π(SPathsβπΊ)β¨βπππββ©)) |
102 | 101 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β (π = β¨βπππββ© β π(SPathsβπΊ)β¨βπππββ©)) |
103 | 102 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β π(SPathsβπΊ)β¨βπππββ©) |
104 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β (β¨βπππββ©β0) = π) |
105 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπ) =
2 β (β¨βπππββ©β(β―βπ)) = (β¨βπππββ©β2)) |
106 | 105, 54 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ) =
2 β (β¨βπππββ©β(β―βπ)) = π) |
107 | 106 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (β¨βπππββ©β(β―βπ)) = π) |
108 | 107 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β (β¨βπππββ©β(β―βπ)) = π) |
109 | 103, 104,
108 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β (π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π)) |
110 | | wlkiswwlks1 28854 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΊ β UPGraph β (π(WalksβπΊ)π β π β (WWalksβπΊ))) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΊ β UPGraph β§ π β π) β (π(WalksβπΊ)π β π β (WWalksβπΊ))) |
112 | 111 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (π(WalksβπΊ)π β π β (WWalksβπΊ))) |
113 | 72, 112 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π(SPathsβπΊ)π β (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β π β (WWalksβπΊ))) |
114 | 113 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β π β (WWalksβπΊ))) |
115 | 114 | impcom 409 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β π β (WWalksβπΊ)) |
116 | 115 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β π β (WWalksβπΊ)) |
117 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β¨βπππββ© β (π β (WWalksβπΊ) β β¨βπππββ© β (WWalksβπΊ))) |
118 | 117 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β¨βπππββ© β (β¨βπππββ© β (WWalksβπΊ) β π β (WWalksβπΊ))) |
119 | 118 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β (β¨βπππββ© β (WWalksβπΊ) β π β (WWalksβπΊ))) |
120 | 116, 119 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β β¨βπππββ© β (WWalksβπΊ)) |
121 | | s3len 14789 |
. . . . . . . . . . . . . . . . . . 19
β’
(β―ββ¨βπππββ©) = 3 |
122 | | df-3 12222 |
. . . . . . . . . . . . . . . . . . 19
β’ 3 = (2 +
1) |
123 | 121, 122 | eqtri 2761 |
. . . . . . . . . . . . . . . . . 18
β’
(β―ββ¨βπππββ©) = (2 + 1) |
124 | 120, 123 | jctir 522 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β (β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1))) |
125 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β (β¨βπππββ©β2) = π) |
126 | 124, 104,
125 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) |
127 | 109, 126 | jca 513 |
. . . . . . . . . . . . . . 15
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β§ π = β¨βπππββ©) β ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) |
128 | 99, 127 | mpdan 686 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ (π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) β ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π))) |
129 | 128 | ex 414 |
. . . . . . . . . . . . 13
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β ((π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)))) |
130 | 129 | exlimdv 1937 |
. . . . . . . . . . . 12
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (βπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β ((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)))) |
131 | 71, 130 | impbid 211 |
. . . . . . . . . . 11
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) β βπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
132 | 131 | adantr 482 |
. . . . . . . . . 10
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (((π(SPathsβπΊ)β¨βπππββ© β§ (β¨βπππββ©β0) = π β§ (β¨βπππββ©β(β―βπ)) = π) β§ ((β¨βπππββ© β (WWalksβπΊ) β§
(β―ββ¨βπππββ©) = (2 + 1)) β§
(β¨βπππββ©β0) = π β§ (β¨βπππββ©β2) = π)) β βπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
133 | 27, 132 | bitrd 279 |
. . . . . . . . 9
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β ((π(π(SPathsOnβπΊ)π)β¨βπππββ© β§ β¨βπππββ© β (π(2 WWalksNOn πΊ)π)) β βπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
134 | 133 | exbidv 1925 |
. . . . . . . 8
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (βπ(π(π(SPathsOnβπΊ)π)β¨βπππββ© β§ β¨βπππββ© β (π(2 WWalksNOn πΊ)π)) β βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
135 | 11, 134 | bitrid 283 |
. . . . . . 7
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β ((β¨βπππββ© β (π(2 WWalksNOn πΊ)π) β§ βπ π(π(SPathsOnβπΊ)π)β¨βπππββ©) β βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
136 | 8, 135 | bitrid 283 |
. . . . . 6
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (β¨βπππββ© β (π(2 WSPathsNOn πΊ)π) β βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
137 | 136 | pm5.32da 580 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β ((π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π)) β (π = β¨βπππββ© β§ βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |
138 | 137 | 2rexbidva 3208 |
. . . 4
β’ ((πΊ β UPGraph β§ π β π) β (βπ β π βπ β π (π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π)) β βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |
139 | 7, 138 | bitrid 283 |
. . 3
β’ ((πΊ β UPGraph β§ π β π) β (βπ β π βπ β π (π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π)) β βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |
140 | 139 | rexbidva 3170 |
. 2
β’ (πΊ β UPGraph β
(βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ β¨βπππββ© β (π(2 WSPathsNOn πΊ)π)) β βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |
141 | 3, 6, 140 | 3bitrd 305 |
1
β’ (πΊ β UPGraph β (π β (2 WSPathsN πΊ) β βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |