Step | Hyp | Ref
| Expression |
1 | | wspthsn 29357 |
. 2
β’ (π WSPathsN πΊ) = {π€ β (π WWalksN πΊ) β£ βπ π(SPathsβπΊ)π€} |
2 | | wwlknbp1 29353 |
. . . . . 6
β’ (π€ β (π WWalksN πΊ) β (π β β0 β§ π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1))) |
3 | | wspn0.v |
. . . . . . . . . . . . 13
β’ π = (VtxβπΊ) |
4 | 3 | eqeq1i 2737 |
. . . . . . . . . . . 12
β’ (π = β
β
(VtxβπΊ) =
β
) |
5 | | wrdeq 14490 |
. . . . . . . . . . . 12
β’
((VtxβπΊ) =
β
β Word (VtxβπΊ) = Word β
) |
6 | 4, 5 | sylbi 216 |
. . . . . . . . . . 11
β’ (π = β
β Word
(VtxβπΊ) = Word
β
) |
7 | 6 | eleq2d 2819 |
. . . . . . . . . 10
β’ (π = β
β (π€ β Word (VtxβπΊ) β π€ β Word β
)) |
8 | | 0wrd0 14494 |
. . . . . . . . . 10
β’ (π€ β Word β
β
π€ =
β
) |
9 | 7, 8 | bitrdi 286 |
. . . . . . . . 9
β’ (π = β
β (π€ β Word (VtxβπΊ) β π€ = β
)) |
10 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
β’ (π€ = β
β
(β―βπ€) =
(β―ββ
)) |
11 | | hash0 14331 |
. . . . . . . . . . . . . . 15
β’
(β―ββ
) = 0 |
12 | 10, 11 | eqtrdi 2788 |
. . . . . . . . . . . . . 14
β’ (π€ = β
β
(β―βπ€) =
0) |
13 | 12 | eqeq1d 2734 |
. . . . . . . . . . . . 13
β’ (π€ = β
β
((β―βπ€) = (π + 1) β 0 = (π + 1))) |
14 | 13 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π€ = β
) β
((β―βπ€) = (π + 1) β 0 = (π + 1))) |
15 | | nn0p1gt0 12505 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β 0 < (π +
1)) |
16 | 15 | gt0ne0d 11782 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 1) β
0) |
17 | | eqneqall 2951 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) = 0 β ((π + 1) β 0 β Β¬
βπ π(SPathsβπΊ)π€)) |
18 | 17 | eqcoms 2740 |
. . . . . . . . . . . . . 14
β’ (0 =
(π + 1) β ((π + 1) β 0 β Β¬
βπ π(SPathsβπΊ)π€)) |
19 | 16, 18 | syl5com 31 |
. . . . . . . . . . . . 13
β’ (π β β0
β (0 = (π + 1) β
Β¬ βπ π(SPathsβπΊ)π€)) |
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π€ = β
) β
(0 = (π + 1) β Β¬
βπ π(SPathsβπΊ)π€)) |
21 | 14, 20 | sylbid 239 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π€ = β
) β
((β―βπ€) = (π + 1) β Β¬ βπ π(SPathsβπΊ)π€)) |
22 | 21 | expcom 414 |
. . . . . . . . . 10
β’ (π€ = β
β (π β β0
β ((β―βπ€) =
(π + 1) β Β¬
βπ π(SPathsβπΊ)π€))) |
23 | 22 | com23 86 |
. . . . . . . . 9
β’ (π€ = β
β
((β―βπ€) = (π + 1) β (π β β0 β Β¬
βπ π(SPathsβπΊ)π€))) |
24 | 9, 23 | syl6bi 252 |
. . . . . . . 8
β’ (π = β
β (π€ β Word (VtxβπΊ) β ((β―βπ€) = (π + 1) β (π β β0 β Β¬
βπ π(SPathsβπΊ)π€)))) |
25 | 24 | com14 96 |
. . . . . . 7
β’ (π β β0
β (π€ β Word
(VtxβπΊ) β
((β―βπ€) = (π + 1) β (π = β
β Β¬ βπ π(SPathsβπΊ)π€)))) |
26 | 25 | 3imp 1111 |
. . . . . 6
β’ ((π β β0
β§ π€ β Word
(VtxβπΊ) β§
(β―βπ€) = (π + 1)) β (π = β
β Β¬ βπ π(SPathsβπΊ)π€)) |
27 | 2, 26 | syl 17 |
. . . . 5
β’ (π€ β (π WWalksN πΊ) β (π = β
β Β¬ βπ π(SPathsβπΊ)π€)) |
28 | 27 | impcom 408 |
. . . 4
β’ ((π = β
β§ π€ β (π WWalksN πΊ)) β Β¬ βπ π(SPathsβπΊ)π€) |
29 | 28 | ralrimiva 3146 |
. . 3
β’ (π = β
β βπ€ β (π WWalksN πΊ) Β¬ βπ π(SPathsβπΊ)π€) |
30 | | rabeq0 4384 |
. . 3
β’ ({π€ β (π WWalksN πΊ) β£ βπ π(SPathsβπΊ)π€} = β
β βπ€ β (π WWalksN πΊ) Β¬ βπ π(SPathsβπΊ)π€) |
31 | 29, 30 | sylibr 233 |
. 2
β’ (π = β
β {π€ β (π WWalksN πΊ) β£ βπ π(SPathsβπΊ)π€} = β
) |
32 | 1, 31 | eqtrid 2784 |
1
β’ (π = β
β (π WSPathsN πΊ) = β
) |