Step | Hyp | Ref
| Expression |
1 | | wlkv 28602 |
. . . . 5
β’ (πΉ(WalksβπΊ)π β (πΊ β V β§ πΉ β V β§ π β V)) |
2 | | eqid 2737 |
. . . . . 6
β’
(VtxβπΊ) =
(VtxβπΊ) |
3 | | lfgrwlkprop.i |
. . . . . 6
β’ πΌ = (iEdgβπΊ) |
4 | 2, 3 | iswlk 28600 |
. . . . 5
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) |
5 | 1, 4 | syl 17 |
. . . 4
β’ (πΉ(WalksβπΊ)π β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) |
6 | | ifptru 1075 |
. . . . . . . . . . . 12
β’ ((πβπ) = (πβ(π + 1)) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πΌβ(πΉβπ)) = {(πβπ)})) |
7 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ (((πβπ) = (πβ(π + 1)) β§ (((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ)))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πΌβ(πΉβπ)) = {(πβπ)})) |
8 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) |
9 | | wrdsymbcl 14422 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β Word dom πΌ β§ π β (0..^(β―βπΉ))) β (πΉβπ) β dom πΌ) |
10 | 9 | ad4ant14 751 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β (πΉβπ) β dom πΌ) |
11 | 8, 10 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β (πΌβ(πΉβπ)) β {π₯ β π« π β£ 2 β€ (β―βπ₯)}) |
12 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (πΌβ(πΉβπ)) β (β―βπ₯) = (β―β(πΌβ(πΉβπ)))) |
13 | 12 | breq2d 5122 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (πΌβ(πΉβπ)) β (2 β€ (β―βπ₯) β 2 β€
(β―β(πΌβ(πΉβπ))))) |
14 | 13 | elrab 3650 |
. . . . . . . . . . . . . 14
β’ ((πΌβ(πΉβπ)) β {π₯ β π« π β£ 2 β€ (β―βπ₯)} β ((πΌβ(πΉβπ)) β π« π β§ 2 β€ (β―β(πΌβ(πΉβπ))))) |
15 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΌβ(πΉβπ)) = {(πβπ)} β (β―β(πΌβ(πΉβπ))) = (β―β{(πβπ)})) |
16 | 15 | breq2d 5122 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌβ(πΉβπ)) = {(πβπ)} β (2 β€ (β―β(πΌβ(πΉβπ))) β 2 β€ (β―β{(πβπ)}))) |
17 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβπ) β V |
18 | | hashsng 14276 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβπ) β V β (β―β{(πβπ)}) = 1) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β―β{(πβπ)}) = 1 |
20 | 19 | breq2i 5118 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 β€
(β―β{(πβπ)}) β 2 β€ 1) |
21 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 <
2 |
22 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 β
β |
23 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
β |
24 | 22, 23 | ltnlei 11283 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 < 2
β Β¬ 2 β€ 1) |
25 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬ 2
β€ 1 β (2 β€ 1 β (πβπ) β (πβ(π + 1)))) |
26 | 24, 25 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1 < 2
β (2 β€ 1 β (πβπ) β (πβ(π + 1)))) |
27 | 21, 26 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 β€ 1
β (πβπ) β (πβ(π + 1))) |
28 | 20, 27 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
β’ (2 β€
(β―β{(πβπ)}) β (πβπ) β (πβ(π + 1))) |
29 | 16, 28 | syl6bi 253 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌβ(πΉβπ)) = {(πβπ)} β (2 β€ (β―β(πΌβ(πΉβπ))) β (πβπ) β (πβ(π + 1)))) |
30 | 29 | com12 32 |
. . . . . . . . . . . . . . . 16
β’ (2 β€
(β―β(πΌβ(πΉβπ))) β ((πΌβ(πΉβπ)) = {(πβπ)} β (πβπ) β (πβ(π + 1)))) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((πΌβ(πΉβπ)) β π« π β§ 2 β€ (β―β(πΌβ(πΉβπ)))) β ((πΌβ(πΉβπ)) = {(πβπ)} β (πβπ) β (πβ(π + 1)))) |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β (((πΌβ(πΉβπ)) β π« π β§ 2 β€ (β―β(πΌβ(πΉβπ)))) β ((πΌβ(πΉβπ)) = {(πβπ)} β (πβπ) β (πβ(π + 1))))) |
33 | 14, 32 | biimtrid 241 |
. . . . . . . . . . . . 13
β’ ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β ((πΌβ(πΉβπ)) β {π₯ β π« π β£ 2 β€ (β―βπ₯)} β ((πΌβ(πΉβπ)) = {(πβπ)} β (πβπ) β (πβ(π + 1))))) |
34 | 11, 33 | mpd 15 |
. . . . . . . . . . . 12
β’ ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β ((πΌβ(πΉβπ)) = {(πβπ)} β (πβπ) β (πβ(π + 1)))) |
35 | 34 | adantl 483 |
. . . . . . . . . . 11
β’ (((πβπ) = (πβ(π + 1)) β§ (((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ)))) β ((πΌβ(πΉβπ)) = {(πβπ)} β (πβπ) β (πβ(π + 1)))) |
36 | 7, 35 | sylbid 239 |
. . . . . . . . . 10
β’ (((πβπ) = (πβ(π + 1)) β§ (((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ)))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πβπ) β (πβ(π + 1)))) |
37 | 36 | ex 414 |
. . . . . . . . 9
β’ ((πβπ) = (πβ(π + 1)) β ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πβπ) β (πβ(π + 1))))) |
38 | | neqne 2952 |
. . . . . . . . . 10
β’ (Β¬
(πβπ) = (πβ(π + 1)) β (πβπ) β (πβ(π + 1))) |
39 | 38 | 2a1d 26 |
. . . . . . . . 9
β’ (Β¬
(πβπ) = (πβ(π + 1)) β ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πβπ) β (πβ(π + 1))))) |
40 | 37, 39 | pm2.61i 182 |
. . . . . . . 8
β’ ((((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β§ π β (0..^(β―βπΉ))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πβπ) β (πβ(π + 1)))) |
41 | 40 | ralimdva 3165 |
. . . . . . 7
β’ (((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1)))) |
42 | 41 | ex 414 |
. . . . . 6
β’ ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β (πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))))) |
43 | 42 | com23 86 |
. . . . 5
β’ ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β βπ β
(0..^(β―βπΉ))(πβπ) β (πβ(π + 1))))) |
44 | 43 | 3impia 1118 |
. . . 4
β’ ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) β (πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β βπ β
(0..^(β―βπΉ))(πβπ) β (πβ(π + 1)))) |
45 | 5, 44 | syl6bi 253 |
. . 3
β’ (πΉ(WalksβπΊ)π β (πΉ(WalksβπΊ)π β (πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β βπ β
(0..^(β―βπΉ))(πβπ) β (πβ(π + 1))))) |
46 | 45 | pm2.43i 52 |
. 2
β’ (πΉ(WalksβπΊ)π β (πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β βπ β
(0..^(β―βπΉ))(πβπ) β (πβ(π + 1)))) |
47 | 46 | imp 408 |
1
β’ ((πΉ(WalksβπΊ)π β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β βπ β
(0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) |