Step | Hyp | Ref
| Expression |
1 | | 1hevtxdg0.i |
. . . 4
β’ (π β (iEdgβπΊ) = {β¨π΄, πΈβ©}) |
2 | 1 | dmeqd 5906 |
. . 3
β’ (π β dom (iEdgβπΊ) = dom {β¨π΄, πΈβ©}) |
3 | | 1hevtxdg1.e |
. . . 4
β’ (π β πΈ β π« π) |
4 | | dmsnopg 6213 |
. . . 4
β’ (πΈ β π« π β dom {β¨π΄, πΈβ©} = {π΄}) |
5 | 3, 4 | syl 17 |
. . 3
β’ (π β dom {β¨π΄, πΈβ©} = {π΄}) |
6 | 2, 5 | eqtrd 2773 |
. 2
β’ (π β dom (iEdgβπΊ) = {π΄}) |
7 | | 1hevtxdg0.a |
. . . . . . 7
β’ (π β π΄ β π) |
8 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = πΈ β (β―βπ₯) = (β―βπΈ)) |
9 | 8 | breq2d 5161 |
. . . . . . . 8
β’ (π₯ = πΈ β (2 β€ (β―βπ₯) β 2 β€
(β―βπΈ))) |
10 | | 1hevtxdg0.v |
. . . . . . . . . 10
β’ (π β (VtxβπΊ) = π) |
11 | 10 | pweqd 4620 |
. . . . . . . . 9
β’ (π β π« (VtxβπΊ) = π« π) |
12 | 3, 11 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β πΈ β π« (VtxβπΊ)) |
13 | | 1hevtxdg1.l |
. . . . . . . 8
β’ (π β 2 β€
(β―βπΈ)) |
14 | 9, 12, 13 | elrabd 3686 |
. . . . . . 7
β’ (π β πΈ β {π₯ β π« (VtxβπΊ) β£ 2 β€
(β―βπ₯)}) |
15 | 7, 14 | fsnd 6877 |
. . . . . 6
β’ (π β {β¨π΄, πΈβ©}:{π΄}βΆ{π₯ β π« (VtxβπΊ) β£ 2 β€
(β―βπ₯)}) |
16 | 15 | adantr 482 |
. . . . 5
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β {β¨π΄, πΈβ©}:{π΄}βΆ{π₯ β π« (VtxβπΊ) β£ 2 β€
(β―βπ₯)}) |
17 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β (iEdgβπΊ) = {β¨π΄, πΈβ©}) |
18 | | simpr 486 |
. . . . . 6
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β dom (iEdgβπΊ) = {π΄}) |
19 | 17, 18 | feq12d 6706 |
. . . . 5
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β ((iEdgβπΊ):dom (iEdgβπΊ)βΆ{π₯ β π« (VtxβπΊ) β£ 2 β€
(β―βπ₯)} β
{β¨π΄, πΈβ©}:{π΄}βΆ{π₯ β π« (VtxβπΊ) β£ 2 β€
(β―βπ₯)})) |
20 | 16, 19 | mpbird 257 |
. . . 4
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β (iEdgβπΊ):dom (iEdgβπΊ)βΆ{π₯ β π« (VtxβπΊ) β£ 2 β€
(β―βπ₯)}) |
21 | | 1hevtxdg0.d |
. . . . . 6
β’ (π β π· β π) |
22 | 21, 10 | eleqtrrd 2837 |
. . . . 5
β’ (π β π· β (VtxβπΊ)) |
23 | 22 | adantr 482 |
. . . 4
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β π· β (VtxβπΊ)) |
24 | | eqid 2733 |
. . . . 5
β’
(VtxβπΊ) =
(VtxβπΊ) |
25 | | eqid 2733 |
. . . . 5
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
26 | | eqid 2733 |
. . . . 5
β’ dom
(iEdgβπΊ) = dom
(iEdgβπΊ) |
27 | | eqid 2733 |
. . . . 5
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
28 | 24, 25, 26, 27 | vtxdlfgrval 28742 |
. . . 4
β’
(((iEdgβπΊ):dom
(iEdgβπΊ)βΆ{π₯ β π« (VtxβπΊ) β£ 2 β€
(β―βπ₯)} β§
π· β (VtxβπΊ)) β ((VtxDegβπΊ)βπ·) = (β―β{π₯ β dom (iEdgβπΊ) β£ π· β ((iEdgβπΊ)βπ₯)})) |
29 | 20, 23, 28 | syl2anc 585 |
. . 3
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β ((VtxDegβπΊ)βπ·) = (β―β{π₯ β dom (iEdgβπΊ) β£ π· β ((iEdgβπΊ)βπ₯)})) |
30 | | rabeq 3447 |
. . . . 5
β’ (dom
(iEdgβπΊ) = {π΄} β {π₯ β dom (iEdgβπΊ) β£ π· β ((iEdgβπΊ)βπ₯)} = {π₯ β {π΄} β£ π· β ((iEdgβπΊ)βπ₯)}) |
31 | 30 | adantl 483 |
. . . 4
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β {π₯ β dom (iEdgβπΊ) β£ π· β ((iEdgβπΊ)βπ₯)} = {π₯ β {π΄} β£ π· β ((iEdgβπΊ)βπ₯)}) |
32 | 31 | fveq2d 6896 |
. . 3
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β (β―β{π₯ β dom (iEdgβπΊ) β£ π· β ((iEdgβπΊ)βπ₯)}) = (β―β{π₯ β {π΄} β£ π· β ((iEdgβπΊ)βπ₯)})) |
33 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = π΄ β ((iEdgβπΊ)βπ₯) = ((iEdgβπΊ)βπ΄)) |
34 | 33 | eleq2d 2820 |
. . . . . . . 8
β’ (π₯ = π΄ β (π· β ((iEdgβπΊ)βπ₯) β π· β ((iEdgβπΊ)βπ΄))) |
35 | 34 | rabsnif 4728 |
. . . . . . 7
β’ {π₯ β {π΄} β£ π· β ((iEdgβπΊ)βπ₯)} = if(π· β ((iEdgβπΊ)βπ΄), {π΄}, β
) |
36 | | 1hevtxdg1.n |
. . . . . . . . 9
β’ (π β π· β πΈ) |
37 | 1 | fveq1d 6894 |
. . . . . . . . . 10
β’ (π β ((iEdgβπΊ)βπ΄) = ({β¨π΄, πΈβ©}βπ΄)) |
38 | | fvsng 7178 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ πΈ β π« π) β ({β¨π΄, πΈβ©}βπ΄) = πΈ) |
39 | 7, 3, 38 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ({β¨π΄, πΈβ©}βπ΄) = πΈ) |
40 | 37, 39 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β ((iEdgβπΊ)βπ΄) = πΈ) |
41 | 36, 40 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β π· β ((iEdgβπΊ)βπ΄)) |
42 | 41 | iftrued 4537 |
. . . . . . 7
β’ (π β if(π· β ((iEdgβπΊ)βπ΄), {π΄}, β
) = {π΄}) |
43 | 35, 42 | eqtrid 2785 |
. . . . . 6
β’ (π β {π₯ β {π΄} β£ π· β ((iEdgβπΊ)βπ₯)} = {π΄}) |
44 | 43 | fveq2d 6896 |
. . . . 5
β’ (π β (β―β{π₯ β {π΄} β£ π· β ((iEdgβπΊ)βπ₯)}) = (β―β{π΄})) |
45 | | hashsng 14329 |
. . . . . 6
β’ (π΄ β π β (β―β{π΄}) = 1) |
46 | 7, 45 | syl 17 |
. . . . 5
β’ (π β (β―β{π΄}) = 1) |
47 | 44, 46 | eqtrd 2773 |
. . . 4
β’ (π β (β―β{π₯ β {π΄} β£ π· β ((iEdgβπΊ)βπ₯)}) = 1) |
48 | 47 | adantr 482 |
. . 3
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β (β―β{π₯ β {π΄} β£ π· β ((iEdgβπΊ)βπ₯)}) = 1) |
49 | 29, 32, 48 | 3eqtrd 2777 |
. 2
β’ ((π β§ dom (iEdgβπΊ) = {π΄}) β ((VtxDegβπΊ)βπ·) = 1) |
50 | 6, 49 | mpdan 686 |
1
β’ (π β ((VtxDegβπΊ)βπ·) = 1) |