Step | Hyp | Ref
| Expression |
1 | | cyclispth 28842 |
. . . . . . . . . . . 12
β’ (π(CyclesβπΊ)π β π(PathsβπΊ)π) |
2 | | acycgrv.1 |
. . . . . . . . . . . . 13
β’ π = (VtxβπΊ) |
3 | 2 | pthhashvtx 33842 |
. . . . . . . . . . . 12
β’ (π(PathsβπΊ)π β (β―βπ) β€ (β―βπ)) |
4 | 1, 3 | syl 17 |
. . . . . . . . . . 11
β’ (π(CyclesβπΊ)π β (β―βπ) β€ (β―βπ)) |
5 | 4 | adantr 481 |
. . . . . . . . . 10
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β (β―βπ) β€ (β―βπ)) |
6 | | breq2 5129 |
. . . . . . . . . . 11
β’
((β―βπ) =
1 β ((β―βπ)
β€ (β―βπ)
β (β―βπ)
β€ 1)) |
7 | 6 | adantl 482 |
. . . . . . . . . 10
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β ((β―βπ) β€ (β―βπ) β (β―βπ) β€ 1)) |
8 | 5, 7 | mpbid 231 |
. . . . . . . . 9
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β (β―βπ) β€ 1) |
9 | 8 | 3adant1 1130 |
. . . . . . . 8
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 1) β (β―βπ) β€ 1) |
10 | | umgrn1cycl 28849 |
. . . . . . . . . 10
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π) β (β―βπ) β 1) |
11 | 10 | 3adant3 1132 |
. . . . . . . . 9
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 1) β (β―βπ) β 1) |
12 | 11 | necomd 2995 |
. . . . . . . 8
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 1) β 1 β (β―βπ)) |
13 | | cycliswlk 28843 |
. . . . . . . . . 10
β’ (π(CyclesβπΊ)π β π(WalksβπΊ)π) |
14 | | wlkcl 28660 |
. . . . . . . . . . . 12
β’ (π(WalksβπΊ)π β (β―βπ) β
β0) |
15 | 14 | nn0red 12498 |
. . . . . . . . . . 11
β’ (π(WalksβπΊ)π β (β―βπ) β β) |
16 | | 1red 11180 |
. . . . . . . . . . 11
β’ (π(WalksβπΊ)π β 1 β β) |
17 | 15, 16 | ltlend 11324 |
. . . . . . . . . 10
β’ (π(WalksβπΊ)π β ((β―βπ) < 1 β ((β―βπ) β€ 1 β§ 1 β
(β―βπ)))) |
18 | 13, 17 | syl 17 |
. . . . . . . . 9
β’ (π(CyclesβπΊ)π β ((β―βπ) < 1 β ((β―βπ) β€ 1 β§ 1 β
(β―βπ)))) |
19 | 18 | 3ad2ant2 1134 |
. . . . . . . 8
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 1) β ((β―βπ) < 1 β
((β―βπ) β€ 1
β§ 1 β (β―βπ)))) |
20 | 9, 12, 19 | mpbir2and 711 |
. . . . . . 7
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 1) β (β―βπ) < 1) |
21 | | nn0lt10b 12589 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β ((β―βπ) < 1 β (β―βπ) = 0)) |
22 | 13, 14, 21 | 3syl 18 |
. . . . . . . 8
β’ (π(CyclesβπΊ)π β ((β―βπ) < 1 β (β―βπ) = 0)) |
23 | 22 | 3ad2ant2 1134 |
. . . . . . 7
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 1) β ((β―βπ) < 1 β
(β―βπ) =
0)) |
24 | 20, 23 | mpbid 231 |
. . . . . 6
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 1) β (β―βπ) = 0) |
25 | | hasheq0 14288 |
. . . . . . 7
β’ (π β V β
((β―βπ) = 0
β π =
β
)) |
26 | 25 | elv 3465 |
. . . . . 6
β’
((β―βπ) =
0 β π =
β
) |
27 | 24, 26 | sylib 217 |
. . . . 5
β’ ((πΊ β UMGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 1) β π = β
) |
28 | 27 | 3com23 1126 |
. . . 4
β’ ((πΊ β UMGraph β§
(β―βπ) = 1 β§
π(CyclesβπΊ)π) β π = β
) |
29 | 28 | 3expia 1121 |
. . 3
β’ ((πΊ β UMGraph β§
(β―βπ) = 1)
β (π(CyclesβπΊ)π β π = β
)) |
30 | 29 | alrimivv 1931 |
. 2
β’ ((πΊ β UMGraph β§
(β―βπ) = 1)
β βπβπ(π(CyclesβπΊ)π β π = β
)) |
31 | | isacycgr1 33861 |
. . 3
β’ (πΊ β UMGraph β (πΊ β AcyclicGraph β
βπβπ(π(CyclesβπΊ)π β π = β
))) |
32 | 31 | adantr 481 |
. 2
β’ ((πΊ β UMGraph β§
(β―βπ) = 1)
β (πΊ β
AcyclicGraph β βπβπ(π(CyclesβπΊ)π β π = β
))) |
33 | 30, 32 | mpbird 256 |
1
β’ ((πΊ β UMGraph β§
(β―βπ) = 1)
β πΊ β
AcyclicGraph) |