| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2732 |
. . . . . 6
β’
(VtxβπΊ) =
(VtxβπΊ) |
| 2 | 1 | clwwlkbp 29227 |
. . . . 5
β’ (π β (ClWWalksβπΊ) β (πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
)) |
| 3 | 2 | adantl 482 |
. . . 4
β’ ((πΊ β UMGraph β§ π β (ClWWalksβπΊ)) β (πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
)) |
| 4 | | lencl 14479 |
. . . . . . 7
β’ (π β Word (VtxβπΊ) β (β―βπ) β
β0) |
| 5 | 4 | 3ad2ant2 1134 |
. . . . . 6
β’ ((πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
) β (β―βπ) β
β0) |
| 6 | 5 | adantl 482 |
. . . . 5
β’ (((πΊ β UMGraph β§ π β (ClWWalksβπΊ)) β§ (πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
)) β (β―βπ) β
β0) |
| 7 | | hasheq0 14319 |
. . . . . . . . . . 11
β’ (π β Word (VtxβπΊ) β ((β―βπ) = 0 β π = β
)) |
| 8 | 7 | bicomd 222 |
. . . . . . . . . 10
β’ (π β Word (VtxβπΊ) β (π = β
β (β―βπ) = 0)) |
| 9 | 8 | necon3bid 2985 |
. . . . . . . . 9
β’ (π β Word (VtxβπΊ) β (π β β
β (β―βπ) β 0)) |
| 10 | 9 | biimpd 228 |
. . . . . . . 8
β’ (π β Word (VtxβπΊ) β (π β β
β (β―βπ) β 0)) |
| 11 | 10 | a1i 11 |
. . . . . . 7
β’ (πΊ β V β (π β Word (VtxβπΊ) β (π β β
β (β―βπ) β 0))) |
| 12 | 11 | 3imp 1111 |
. . . . . 6
β’ ((πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
) β (β―βπ) β 0) |
| 13 | 12 | adantl 482 |
. . . . 5
β’ (((πΊ β UMGraph β§ π β (ClWWalksβπΊ)) β§ (πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
)) β (β―βπ) β 0) |
| 14 | | clwwlk1loop 29230 |
. . . . . . . . . 10
β’ ((π β (ClWWalksβπΊ) β§ (β―βπ) = 1) β {(πβ0), (πβ0)} β (EdgβπΊ)) |
| 15 | 14 | expcom 414 |
. . . . . . . . 9
β’
((β―βπ) =
1 β (π β
(ClWWalksβπΊ) β
{(πβ0), (πβ0)} β
(EdgβπΊ))) |
| 16 | | eqid 2732 |
. . . . . . . . . . 11
β’ (πβ0) = (πβ0) |
| 17 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(EdgβπΊ) =
(EdgβπΊ) |
| 18 | 17 | umgredgne 28394 |
. . . . . . . . . . 11
β’ ((πΊ β UMGraph β§ {(πβ0), (πβ0)} β (EdgβπΊ)) β (πβ0) β (πβ0)) |
| 19 | | eqneqall 2951 |
. . . . . . . . . . 11
β’ ((πβ0) = (πβ0) β ((πβ0) β (πβ0) β ((πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
) β (β―βπ) β 1))) |
| 20 | 16, 18, 19 | mpsyl 68 |
. . . . . . . . . 10
β’ ((πΊ β UMGraph β§ {(πβ0), (πβ0)} β (EdgβπΊ)) β ((πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
) β (β―βπ) β 1)) |
| 21 | 20 | expcom 414 |
. . . . . . . . 9
β’ ({(πβ0), (πβ0)} β (EdgβπΊ) β (πΊ β UMGraph β ((πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
) β (β―βπ) β 1))) |
| 22 | 15, 21 | syl6 35 |
. . . . . . . 8
β’
((β―βπ) =
1 β (π β
(ClWWalksβπΊ) β
(πΊ β UMGraph β
((πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
) β (β―βπ) β 1)))) |
| 23 | 22 | com23 86 |
. . . . . . 7
β’
((β―βπ) =
1 β (πΊ β UMGraph
β (π β
(ClWWalksβπΊ) β
((πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
) β (β―βπ) β 1)))) |
| 24 | 23 | imp4c 424 |
. . . . . 6
β’
((β―βπ) =
1 β (((πΊ β
UMGraph β§ π β
(ClWWalksβπΊ)) β§
(πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
)) β (β―βπ) β 1)) |
| 25 | | neqne 2948 |
. . . . . . 7
β’ (Β¬
(β―βπ) = 1
β (β―βπ)
β 1) |
| 26 | 25 | a1d 25 |
. . . . . 6
β’ (Β¬
(β―βπ) = 1
β (((πΊ β UMGraph
β§ π β
(ClWWalksβπΊ)) β§
(πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
)) β (β―βπ) β 1)) |
| 27 | 24, 26 | pm2.61i 182 |
. . . . 5
β’ (((πΊ β UMGraph β§ π β (ClWWalksβπΊ)) β§ (πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
)) β (β―βπ) β 1) |
| 28 | 6, 13, 27 | 3jca 1128 |
. . . 4
β’ (((πΊ β UMGraph β§ π β (ClWWalksβπΊ)) β§ (πΊ β V β§ π β Word (VtxβπΊ) β§ π β β
)) β ((β―βπ) β β0
β§ (β―βπ)
β 0 β§ (β―βπ) β 1)) |
| 29 | 3, 28 | mpdan 685 |
. . 3
β’ ((πΊ β UMGraph β§ π β (ClWWalksβπΊ)) β ((β―βπ) β β0
β§ (β―βπ)
β 0 β§ (β―βπ) β 1)) |
| 30 | | nn0n0n1ge2 12535 |
. . 3
β’
(((β―βπ)
β β0 β§ (β―βπ) β 0 β§ (β―βπ) β 1) β 2 β€
(β―βπ)) |
| 31 | 29, 30 | syl 17 |
. 2
β’ ((πΊ β UMGraph β§ π β (ClWWalksβπΊ)) β 2 β€
(β―βπ)) |
| 32 | 31 | ex 413 |
1
β’ (πΊ β UMGraph β (π β (ClWWalksβπΊ) β 2 β€
(β―βπ))) |
