Step | Hyp | Ref
| Expression |
1 | | hashfz0 14341 |
. . . 4
β’
(((β―βπΉ)
β 1) β β0 β
(β―β(0...((β―βπΉ) β 1))) = (((β―βπΉ) β 1) +
1)) |
2 | | pthiswlk 28724 |
. . . . . 6
β’ (πΉ(PathsβπΊ)π β πΉ(WalksβπΊ)π) |
3 | | wlkcl 28612 |
. . . . . 6
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) β
β0) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ (πΉ(PathsβπΊ)π β (β―βπΉ) β
β0) |
5 | | nn0cn 12431 |
. . . . 5
β’
((β―βπΉ)
β β0 β (β―βπΉ) β β) |
6 | | npcan1 11588 |
. . . . 5
β’
((β―βπΉ)
β β β (((β―βπΉ) β 1) + 1) = (β―βπΉ)) |
7 | 4, 5, 6 | 3syl 18 |
. . . 4
β’ (πΉ(PathsβπΊ)π β (((β―βπΉ) β 1) + 1) = (β―βπΉ)) |
8 | 1, 7 | sylan9eqr 2795 |
. . 3
β’ ((πΉ(PathsβπΊ)π β§ ((β―βπΉ) β 1) β β0)
β (β―β(0...((β―βπΉ) β 1))) = (β―βπΉ)) |
9 | | pthhashvtx.1 |
. . . . . . . 8
β’ π = (VtxβπΊ) |
10 | 9 | wlkp 28613 |
. . . . . . 7
β’ (πΉ(WalksβπΊ)π β π:(0...(β―βπΉ))βΆπ) |
11 | 2, 10 | syl 17 |
. . . . . 6
β’ (πΉ(PathsβπΊ)π β π:(0...(β―βπΉ))βΆπ) |
12 | 11 | ffnd 6673 |
. . . . 5
β’ (πΉ(PathsβπΊ)π β π Fn (0...(β―βπΉ))) |
13 | | fzfi 13886 |
. . . . 5
β’
(0...((β―βπΉ) β 1)) β Fin |
14 | | resfnfinfin 9282 |
. . . . 5
β’ ((π Fn (0...(β―βπΉ)) β§
(0...((β―βπΉ)
β 1)) β Fin) β (π βΎ (0...((β―βπΉ) β 1))) β
Fin) |
15 | 12, 13, 14 | sylancl 587 |
. . . 4
β’ (πΉ(PathsβπΊ)π β (π βΎ (0...((β―βπΉ) β 1))) β
Fin) |
16 | | simpr 486 |
. . . . 5
β’ ((πΉ(PathsβπΊ)π β§ ((β―βπΉ) β 1) β β0)
β ((β―βπΉ)
β 1) β β0) |
17 | | fzssp1 13493 |
. . . . . . . 8
β’
(0...((β―βπΉ) β 1)) β
(0...(((β―βπΉ)
β 1) + 1)) |
18 | 7 | oveq2d 7377 |
. . . . . . . 8
β’ (πΉ(PathsβπΊ)π β (0...(((β―βπΉ) β 1) + 1)) =
(0...(β―βπΉ))) |
19 | 17, 18 | sseqtrid 4000 |
. . . . . . 7
β’ (πΉ(PathsβπΊ)π β (0...((β―βπΉ) β 1)) β
(0...(β―βπΉ))) |
20 | 11, 19 | fssresd 6713 |
. . . . . 6
β’ (πΉ(PathsβπΊ)π β (π βΎ (0...((β―βπΉ) β
1))):(0...((β―βπΉ) β 1))βΆπ) |
21 | 20 | adantr 482 |
. . . . 5
β’ ((πΉ(PathsβπΊ)π β§ ((β―βπΉ) β 1) β β0)
β (π βΎ
(0...((β―βπΉ)
β 1))):(0...((β―βπΉ) β 1))βΆπ) |
22 | | fz1ssfz0 13546 |
. . . . . . . . 9
β’
(1...((β―βπΉ) β 1)) β
(0...((β―βπΉ)
β 1)) |
23 | 22 | a1i 11 |
. . . . . . . 8
β’ (πΉ(PathsβπΊ)π β (1...((β―βπΉ) β 1)) β
(0...((β―βπΉ)
β 1))) |
24 | 20, 23 | fssresd 6713 |
. . . . . . 7
β’ (πΉ(PathsβπΊ)π β ((π βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1))):(1...((β―βπΉ) β 1))βΆπ) |
25 | | ispth 28720 |
. . . . . . . . 9
β’ (πΉ(PathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) =
β
)) |
26 | 25 | simp2bi 1147 |
. . . . . . . 8
β’ (πΉ(PathsβπΊ)π β Fun β‘(π βΎ (1..^(β―βπΉ)))) |
27 | | nn0z 12532 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ)
β β0 β (β―βπΉ) β β€) |
28 | | fzoval 13582 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ)
β β€ β (1..^(β―βπΉ)) = (1...((β―βπΉ) β 1))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . 13
β’
((β―βπΉ)
β β0 β (1..^(β―βπΉ)) = (1...((β―βπΉ) β 1))) |
30 | 4, 29 | syl 17 |
. . . . . . . . . . . 12
β’ (πΉ(PathsβπΊ)π β (1..^(β―βπΉ)) = (1...((β―βπΉ) β 1))) |
31 | 30 | reseq2d 5941 |
. . . . . . . . . . 11
β’ (πΉ(PathsβπΊ)π β (π βΎ (1..^(β―βπΉ))) = (π βΎ (1...((β―βπΉ) β 1)))) |
32 | | resabs1 5971 |
. . . . . . . . . . . 12
β’
((1...((β―βπΉ) β 1)) β
(0...((β―βπΉ)
β 1)) β ((π
βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1))) = (π βΎ
(1...((β―βπΉ)
β 1)))) |
33 | 22, 32 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π βΎ
(0...((β―βπΉ)
β 1))) βΎ (1...((β―βπΉ) β 1))) = (π βΎ (1...((β―βπΉ) β 1))) |
34 | 31, 33 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (πΉ(PathsβπΊ)π β (π βΎ (1..^(β―βπΉ))) = ((π βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1)))) |
35 | 34 | cnveqd 5835 |
. . . . . . . . 9
β’ (πΉ(PathsβπΊ)π β β‘(π βΎ (1..^(β―βπΉ))) = β‘((π βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1)))) |
36 | 35 | funeqd 6527 |
. . . . . . . 8
β’ (πΉ(PathsβπΊ)π β (Fun β‘(π βΎ (1..^(β―βπΉ))) β Fun β‘((π βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1))))) |
37 | 26, 36 | mpbid 231 |
. . . . . . 7
β’ (πΉ(PathsβπΊ)π β Fun β‘((π βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1)))) |
38 | | df-f1 6505 |
. . . . . . 7
β’ (((π βΎ
(0...((β―βπΉ)
β 1))) βΎ (1...((β―βπΉ) β 1))):(1...((β―βπΉ) β 1))β1-1βπ β (((π βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1))):(1...((β―βπΉ) β 1))βΆπ β§ Fun β‘((π βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1))))) |
39 | 24, 37, 38 | sylanbrc 584 |
. . . . . 6
β’ (πΉ(PathsβπΊ)π β ((π βΎ (0...((β―βπΉ) β 1))) βΎ
(1...((β―βπΉ)
β 1))):(1...((β―βπΉ) β 1))β1-1βπ) |
40 | 39 | adantr 482 |
. . . . 5
β’ ((πΉ(PathsβπΊ)π β§ ((β―βπΉ) β 1) β β0)
β ((π βΎ
(0...((β―βπΉ)
β 1))) βΎ (1...((β―βπΉ) β 1))):(1...((β―βπΉ) β 1))β1-1βπ) |
41 | | snsspr1 4778 |
. . . . . . . 8
β’ {0}
β {0, (β―βπΉ)} |
42 | | imass2 6058 |
. . . . . . . 8
β’ ({0}
β {0, (β―βπΉ)} β (π β {0}) β (π β {0, (β―βπΉ)})) |
43 | 41, 42 | ax-mp 5 |
. . . . . . 7
β’ (π β {0}) β (π β {0,
(β―βπΉ)}) |
44 | | 0elfz 13547 |
. . . . . . . . 9
β’
(((β―βπΉ)
β 1) β β0 β 0 β
(0...((β―βπΉ)
β 1))) |
45 | 44 | snssd 4773 |
. . . . . . . 8
β’
(((β―βπΉ)
β 1) β β0 β {0} β
(0...((β―βπΉ)
β 1))) |
46 | | resima2 5976 |
. . . . . . . 8
β’ ({0}
β (0...((β―βπΉ) β 1)) β ((π βΎ (0...((β―βπΉ) β 1))) β {0}) =
(π β
{0})) |
47 | | sseq1 3973 |
. . . . . . . 8
β’ (((π βΎ
(0...((β―βπΉ)
β 1))) β {0}) = (π β {0}) β (((π βΎ (0...((β―βπΉ) β 1))) β {0})
β (π β {0,
(β―βπΉ)}) β
(π β {0}) β
(π β {0,
(β―βπΉ)}))) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . 7
β’
(((β―βπΉ)
β 1) β β0 β (((π βΎ (0...((β―βπΉ) β 1))) β {0})
β (π β {0,
(β―βπΉ)}) β
(π β {0}) β
(π β {0,
(β―βπΉ)}))) |
49 | 43, 48 | mpbiri 258 |
. . . . . 6
β’
(((β―βπΉ)
β 1) β β0 β ((π βΎ (0...((β―βπΉ) β 1))) β {0})
β (π β {0,
(β―βπΉ)})) |
50 | | resima2 5976 |
. . . . . . . . . 10
β’
((1...((β―βπΉ) β 1)) β
(0...((β―βπΉ)
β 1)) β ((π
βΎ (0...((β―βπΉ) β 1))) β
(1...((β―βπΉ)
β 1))) = (π β
(1...((β―βπΉ)
β 1)))) |
51 | 22, 50 | ax-mp 5 |
. . . . . . . . 9
β’ ((π βΎ
(0...((β―βπΉ)
β 1))) β (1...((β―βπΉ) β 1))) = (π β (1...((β―βπΉ) β 1))) |
52 | 30 | imaeq2d 6017 |
. . . . . . . . 9
β’ (πΉ(PathsβπΊ)π β (π β (1..^(β―βπΉ))) = (π β (1...((β―βπΉ) β 1)))) |
53 | 51, 52 | eqtr4id 2792 |
. . . . . . . 8
β’ (πΉ(PathsβπΊ)π β ((π βΎ (0...((β―βπΉ) β 1))) β
(1...((β―βπΉ)
β 1))) = (π β
(1..^(β―βπΉ)))) |
54 | 53 | ineq2d 4176 |
. . . . . . 7
β’ (πΉ(PathsβπΊ)π β ((π β {0, (β―βπΉ)}) β© ((π βΎ (0...((β―βπΉ) β 1))) β
(1...((β―βπΉ)
β 1)))) = ((π β
{0, (β―βπΉ)})
β© (π β
(1..^(β―βπΉ))))) |
55 | 25 | simp3bi 1148 |
. . . . . . 7
β’ (πΉ(PathsβπΊ)π β ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) |
56 | 54, 55 | eqtrd 2773 |
. . . . . 6
β’ (πΉ(PathsβπΊ)π β ((π β {0, (β―βπΉ)}) β© ((π βΎ (0...((β―βπΉ) β 1))) β
(1...((β―βπΉ)
β 1)))) = β
) |
57 | | ssdisj 4423 |
. . . . . 6
β’ ((((π βΎ
(0...((β―βπΉ)
β 1))) β {0}) β (π β {0, (β―βπΉ)}) β§ ((π β {0, (β―βπΉ)}) β© ((π βΎ (0...((β―βπΉ) β 1))) β
(1...((β―βπΉ)
β 1)))) = β
) β (((π βΎ (0...((β―βπΉ) β 1))) β {0})
β© ((π βΎ
(0...((β―βπΉ)
β 1))) β (1...((β―βπΉ) β 1)))) = β
) |
58 | 49, 56, 57 | syl2anr 598 |
. . . . 5
β’ ((πΉ(PathsβπΊ)π β§ ((β―βπΉ) β 1) β β0)
β (((π βΎ
(0...((β―βπΉ)
β 1))) β {0}) β© ((π βΎ (0...((β―βπΉ) β 1))) β
(1...((β―βπΉ)
β 1)))) = β
) |
59 | 16, 21, 40, 58 | f1resfz0f1d 33768 |
. . . 4
β’ ((πΉ(PathsβπΊ)π β§ ((β―βπΉ) β 1) β β0)
β (π βΎ
(0...((β―βπΉ)
β 1))):(0...((β―βπΉ) β 1))β1-1βπ) |
60 | 9 | fvexi 6860 |
. . . . 5
β’ π β V |
61 | | hashf1dmcdm 33772 |
. . . . 5
β’ (((π βΎ
(0...((β―βπΉ)
β 1))) β Fin β§ π β V β§ (π βΎ (0...((β―βπΉ) β
1))):(0...((β―βπΉ) β 1))β1-1βπ) β
(β―β(0...((β―βπΉ) β 1))) β€ (β―βπ)) |
62 | 60, 61 | mp3an2 1450 |
. . . 4
β’ (((π βΎ
(0...((β―βπΉ)
β 1))) β Fin β§ (π βΎ (0...((β―βπΉ) β
1))):(0...((β―βπΉ) β 1))β1-1βπ) β
(β―β(0...((β―βπΉ) β 1))) β€ (β―βπ)) |
63 | 15, 59, 62 | syl2an2r 684 |
. . 3
β’ ((πΉ(PathsβπΊ)π β§ ((β―βπΉ) β 1) β β0)
β (β―β(0...((β―βπΉ) β 1))) β€ (β―βπ)) |
64 | 8, 63 | eqbrtrrd 5133 |
. 2
β’ ((πΉ(PathsβπΊ)π β§ ((β―βπΉ) β 1) β β0)
β (β―βπΉ)
β€ (β―βπ)) |
65 | | 0nn0m1nnn0 33767 |
. . . . 5
β’
((β―βπΉ) =
0 β ((β―βπΉ)
β β0 β§ Β¬ ((β―βπΉ) β 1) β
β0)) |
66 | 65 | biimpri 227 |
. . . 4
β’
(((β―βπΉ)
β β0 β§ Β¬ ((β―βπΉ) β 1) β β0)
β (β―βπΉ) =
0) |
67 | 4, 66 | sylan 581 |
. . 3
β’ ((πΉ(PathsβπΊ)π β§ Β¬ ((β―βπΉ) β 1) β
β0) β (β―βπΉ) = 0) |
68 | | hashge0 14296 |
. . . 4
β’ (π β V β 0 β€
(β―βπ)) |
69 | 60, 68 | ax-mp 5 |
. . 3
β’ 0 β€
(β―βπ) |
70 | 67, 69 | eqbrtrdi 5148 |
. 2
β’ ((πΉ(PathsβπΊ)π β§ Β¬ ((β―βπΉ) β 1) β
β0) β (β―βπΉ) β€ (β―βπ)) |
71 | 64, 70 | pm2.61dan 812 |
1
β’ (πΉ(PathsβπΊ)π β (β―βπΉ) β€ (β―βπ)) |