Step | Hyp | Ref
| Expression |
1 | | elwwlks2.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | 1 | wwlksnwwlksnon 28902 |
. . 3
β’ (π β (2 WWalksN πΊ) β βπ β π βπ β π π β (π(2 WWalksNOn πΊ)π)) |
3 | 2 | a1i 11 |
. 2
β’ (πΊ β UPGraph β (π β (2 WWalksN πΊ) β βπ β π βπ β π π β (π(2 WWalksNOn πΊ)π))) |
4 | 1 | elwwlks2on 28946 |
. . . 4
β’ ((πΊ β UPGraph β§ π β π β§ π β π) β (π β (π(2 WWalksNOn πΊ)π) β βπ β π (π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)))) |
5 | 4 | 3expb 1121 |
. . 3
β’ ((πΊ β UPGraph β§ (π β π β§ π β π)) β (π β (π(2 WWalksNOn πΊ)π) β βπ β π (π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)))) |
6 | 5 | 2rexbidva 3208 |
. 2
β’ (πΊ β UPGraph β
(βπ β π βπ β π π β (π(2 WWalksNOn πΊ)π) β βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)))) |
7 | | rexcom 3272 |
. . . 4
β’
(βπ β
π βπ β π (π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)) β βπ β π βπ β π (π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2))) |
8 | | s3cli 14776 |
. . . . . . . . . 10
β’
β¨βπππββ© β Word V |
9 | 8 | a1i 11 |
. . . . . . . . 9
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β β¨βπππββ© β Word V) |
10 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β π = β¨βπππββ©) |
11 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β π = β¨βπππββ©) |
12 | 10, 11 | eqtr4d 2776 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β π = π) |
13 | 12 | breq2d 5118 |
. . . . . . . . . . . . . . 15
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β (π(WalksβπΊ)π β π(WalksβπΊ)π)) |
14 | 13 | biimpd 228 |
. . . . . . . . . . . . . 14
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β (π(WalksβπΊ)π β π(WalksβπΊ)π)) |
15 | 14 | com12 32 |
. . . . . . . . . . . . 13
β’ (π(WalksβπΊ)π β (((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β π(WalksβπΊ)π)) |
16 | 15 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π(WalksβπΊ)π β§ (β―βπ) = 2) β (((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β π(WalksβπΊ)π)) |
17 | 16 | impcom 409 |
. . . . . . . . . . 11
β’
((((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β§ (π(WalksβπΊ)π β§ (β―βπ) = 2)) β π(WalksβπΊ)π) |
18 | | simprr 772 |
. . . . . . . . . . 11
β’
((((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β§ (π(WalksβπΊ)π β§ (β―βπ) = 2)) β (β―βπ) = 2) |
19 | | vex 3448 |
. . . . . . . . . . . . . . . 16
β’ π β V |
20 | | s3fv0 14786 |
. . . . . . . . . . . . . . . . 17
β’ (π β V β
(β¨βπππββ©β0) = π) |
21 | 20 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β V β π = (β¨βπππββ©β0)) |
22 | 19, 21 | mp1i 13 |
. . . . . . . . . . . . . . 15
β’ (π = β¨βπππββ© β π = (β¨βπππββ©β0)) |
23 | | fveq1 6842 |
. . . . . . . . . . . . . . 15
β’ (π = β¨βπππββ© β (πβ0) = (β¨βπππββ©β0)) |
24 | 22, 23 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ (π = β¨βπππββ© β π = (πβ0)) |
25 | | vex 3448 |
. . . . . . . . . . . . . . . 16
β’ π β V |
26 | | s3fv1 14787 |
. . . . . . . . . . . . . . . . 17
β’ (π β V β
(β¨βπππββ©β1) = π) |
27 | 26 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β V β π = (β¨βπππββ©β1)) |
28 | 25, 27 | mp1i 13 |
. . . . . . . . . . . . . . 15
β’ (π = β¨βπππββ© β π = (β¨βπππββ©β1)) |
29 | | fveq1 6842 |
. . . . . . . . . . . . . . 15
β’ (π = β¨βπππββ© β (πβ1) = (β¨βπππββ©β1)) |
30 | 28, 29 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ (π = β¨βπππββ© β π = (πβ1)) |
31 | | vex 3448 |
. . . . . . . . . . . . . . . 16
β’ π β V |
32 | | s3fv2 14788 |
. . . . . . . . . . . . . . . . 17
β’ (π β V β
(β¨βπππββ©β2) = π) |
33 | 32 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β V β π = (β¨βπππββ©β2)) |
34 | 31, 33 | mp1i 13 |
. . . . . . . . . . . . . . 15
β’ (π = β¨βπππββ© β π = (β¨βπππββ©β2)) |
35 | | fveq1 6842 |
. . . . . . . . . . . . . . 15
β’ (π = β¨βπππββ© β (πβ2) = (β¨βπππββ©β2)) |
36 | 34, 35 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ (π = β¨βπππββ© β π = (πβ2)) |
37 | 24, 30, 36 | 3jca 1129 |
. . . . . . . . . . . . 13
β’ (π = β¨βπππββ© β (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) |
38 | 37 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) |
39 | 38 | adantr 482 |
. . . . . . . . . . 11
β’
((((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β§ (π(WalksβπΊ)π β§ (β―βπ) = 2)) β (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) |
40 | 17, 18, 39 | 3jca 1129 |
. . . . . . . . . 10
β’
((((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β§ (π(WalksβπΊ)π β§ (β―βπ) = 2)) β (π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))) |
41 | 40 | ex 414 |
. . . . . . . . 9
β’
(((((πΊ β
UPGraph β§ π β
π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β§ π = β¨βπππββ©) β ((π(WalksβπΊ)π β§ (β―βπ) = 2) β (π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
42 | 9, 41 | spcimedv 3553 |
. . . . . . . 8
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β ((π(WalksβπΊ)π β§ (β―βπ) = 2) β βπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
43 | | wlklenvp1 28608 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π(WalksβπΊ)π β (β―βπ) = ((β―βπ) + 1)) |
44 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπ)
= ((β―βπ) + 1)
β§ (β―βπ) =
2) β (β―βπ)
= ((β―βπ) +
1)) |
45 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((β―βπ) =
2 β ((β―βπ)
+ 1) = (2 + 1)) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπ)
= ((β―βπ) + 1)
β§ (β―βπ) =
2) β ((β―βπ) + 1) = (2 + 1)) |
47 | 44, 46 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((β―βπ)
= ((β―βπ) + 1)
β§ (β―βπ) =
2) β (β―βπ)
= (2 + 1)) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π(WalksβπΊ)π β§ ((β―βπ) = ((β―βπ) + 1) β§ (β―βπ) = 2)) β
(β―βπ) = (2 +
1)) |
49 | | 2p1e3 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (2 + 1) =
3 |
50 | 48, 49 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π(WalksβπΊ)π β§ ((β―βπ) = ((β―βπ) + 1) β§ (β―βπ) = 2)) β
(β―βπ) =
3) |
51 | 50 | exp32 422 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π(WalksβπΊ)π β ((β―βπ) = ((β―βπ) + 1) β ((β―βπ) = 2 β
(β―βπ) =
3))) |
52 | 43, 51 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π(WalksβπΊ)π β ((β―βπ) = 2 β (β―βπ) = 3)) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β ((β―βπ) = 2 β
(β―βπ) =
3)) |
54 | 53 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β
(β―βπ) =
3) |
55 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πβ0) β (πβ0) = π) |
56 | 55 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ0) β (πβ0) = π) |
57 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πβ1) β (πβ1) = π) |
58 | 57 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ1) β (πβ1) = π) |
59 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πβ2) β (πβ2) = π) |
60 | 59 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ2) β (πβ2) = π) |
61 | 56, 58, 60 | 3anim123i 1152 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)) β ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)) |
62 | 54, 61 | anim12i 614 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β ((β―βπ) = 3 β§ ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π))) |
63 | 1 | wlkpwrd 28607 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π(WalksβπΊ)π β π β Word π) |
64 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΊ β UPGraph β§ π β π) β π β π) |
65 | 64 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (π β π β§ (π β π β§ π β π))) |
66 | | 3anass 1096 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π β§ π β π β§ π β π) β (π β π β§ (π β π β§ π β π))) |
67 | 65, 66 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β (π β π β§ π β π β§ π β π)) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (π β π β§ π β π β§ π β π)) |
69 | 63, 68 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β (π β Word π β§ (π β π β§ π β π β§ π β π))) |
70 | 69 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π β Word π β§ (π β π β§ π β π β§ π β π))) |
71 | | eqwrds3 14856 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Word π β§ (π β π β§ π β π β§ π β π)) β (π = β¨βπππββ© β ((β―βπ) = 3 β§ ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)))) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π = β¨βπππββ© β ((β―βπ) = 3 β§ ((πβ0) = π β§ (πβ1) = π β§ (πβ2) = π)))) |
73 | 62, 72 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β π = β¨βπππββ©) |
74 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β π = β¨βπππββ©) |
75 | 74 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β π = β¨βπππββ©) |
76 | 73, 75 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β π = π) |
77 | 76 | breq2d 5118 |
. . . . . . . . . . . . . . . 16
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π(WalksβπΊ)π β π(WalksβπΊ)π)) |
78 | 77 | biimpd 228 |
. . . . . . . . . . . . . . 15
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π(WalksβπΊ)π β π(WalksβπΊ)π)) |
79 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (β―βπ) = 2) |
80 | 78, 79 | jctird 528 |
. . . . . . . . . . . . . 14
β’ ((((π(WalksβπΊ)π β§ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©)) β§ (β―βπ) = 2) β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π(WalksβπΊ)π β (π(WalksβπΊ)π β§ (β―βπ) = 2))) |
81 | 80 | exp41 436 |
. . . . . . . . . . . . 13
β’ (π(WalksβπΊ)π β ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β ((β―βπ) = 2 β ((π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)) β (π(WalksβπΊ)π β (π(WalksβπΊ)π β§ (β―βπ) = 2)))))) |
82 | 81 | com25 99 |
. . . . . . . . . . . 12
β’ (π(WalksβπΊ)π β (π(WalksβπΊ)π β ((β―βπ) = 2 β ((π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)) β ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (π(WalksβπΊ)π β§ (β―βπ) = 2)))))) |
83 | 82 | pm2.43i 52 |
. . . . . . . . . . 11
β’ (π(WalksβπΊ)π β ((β―βπ) = 2 β ((π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)) β ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (π(WalksβπΊ)π β§ (β―βπ) = 2))))) |
84 | 83 | 3imp 1112 |
. . . . . . . . . 10
β’ ((π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (π(WalksβπΊ)π β§ (β―βπ) = 2))) |
85 | 84 | com12 32 |
. . . . . . . . 9
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β ((π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π(WalksβπΊ)π β§ (β―βπ) = 2))) |
86 | 85 | exlimdv 1937 |
. . . . . . . 8
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (βπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))) β (π(WalksβπΊ)π β§ (β―βπ) = 2))) |
87 | 42, 86 | impbid 211 |
. . . . . . 7
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β ((π(WalksβπΊ)π β§ (β―βπ) = 2) β βπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
88 | 87 | exbidv 1925 |
. . . . . 6
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β§ π = β¨βπππββ©) β (βπ(π(WalksβπΊ)π β§ (β―βπ) = 2) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2))))) |
89 | 88 | pm5.32da 580 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β π β§ π β π)) β ((π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)) β (π = β¨βπππββ© β§ βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |
90 | 89 | 2rexbidva 3208 |
. . . 4
β’ ((πΊ β UPGraph β§ π β π) β (βπ β π βπ β π (π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)) β βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |
91 | 7, 90 | bitrid 283 |
. . 3
β’ ((πΊ β UPGraph β§ π β π) β (βπ β π βπ β π (π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)) β βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |
92 | 91 | rexbidva 3170 |
. 2
β’ (πΊ β UPGraph β
(βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)) β βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |
93 | 3, 6, 92 | 3bitrd 305 |
1
β’ (πΊ β UPGraph β (π β (2 WWalksN πΊ) β βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) |