| Step | Hyp | Ref
| Expression |
|---|
| 1 | | vtxdg0e.i |
. . . . 5
β’ πΌ = (iEdgβπΊ) |
| 2 | 1 | eqeq1i 2737 |
. . . 4
β’ (πΌ = β
β
(iEdgβπΊ) =
β
) |
| 3 | | dmeq 5903 |
. . . . . 6
β’
((iEdgβπΊ) =
β
β dom (iEdgβπΊ) = dom β
) |
| 4 | | dm0 5920 |
. . . . . 6
β’ dom
β
= β
|
| 5 | 3, 4 | eqtrdi 2788 |
. . . . 5
β’
((iEdgβπΊ) =
β
β dom (iEdgβπΊ) = β
) |
| 6 | | 0fin 9173 |
. . . . 5
β’ β
β Fin |
| 7 | 5, 6 | eqeltrdi 2841 |
. . . 4
β’
((iEdgβπΊ) =
β
β dom (iEdgβπΊ) β Fin) |
| 8 | 2, 7 | sylbi 216 |
. . 3
β’ (πΌ = β
β dom
(iEdgβπΊ) β
Fin) |
| 9 | | simpl 483 |
. . 3
β’ ((π β π β§ πΌ = β
) β π β π) |
| 10 | | vtxdgf.v |
. . . 4
β’ π = (VtxβπΊ) |
| 11 | | eqid 2732 |
. . . 4
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
| 12 | | eqid 2732 |
. . . 4
β’ dom
(iEdgβπΊ) = dom
(iEdgβπΊ) |
| 13 | 10, 11, 12 | vtxdgfival 28981 |
. . 3
β’ ((dom
(iEdgβπΊ) β Fin
β§ π β π) β ((VtxDegβπΊ)βπ) = ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) + (β―β{π₯ β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ₯) = {π}}))) |
| 14 | 8, 9, 13 | syl2an2 684 |
. 2
β’ ((π β π β§ πΌ = β
) β ((VtxDegβπΊ)βπ) = ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) + (β―β{π₯ β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ₯) = {π}}))) |
| 15 | 2, 5 | sylbi 216 |
. . . . 5
β’ (πΌ = β
β dom
(iEdgβπΊ) =
β
) |
| 16 | 15 | adantl 482 |
. . . 4
β’ ((π β π β§ πΌ = β
) β dom (iEdgβπΊ) = β
) |
| 17 | | rabeq 3446 |
. . . . . . . 8
β’ (dom
(iEdgβπΊ) = β
β {π₯ β dom
(iEdgβπΊ) β£
π β ((iEdgβπΊ)βπ₯)} = {π₯ β β
β£ π β ((iEdgβπΊ)βπ₯)}) |
| 18 | | rab0 4382 |
. . . . . . . 8
β’ {π₯ β β
β£ π β ((iEdgβπΊ)βπ₯)} = β
|
| 19 | 17, 18 | eqtrdi 2788 |
. . . . . . 7
β’ (dom
(iEdgβπΊ) = β
β {π₯ β dom
(iEdgβπΊ) β£
π β ((iEdgβπΊ)βπ₯)} = β
) |
| 20 | 19 | fveq2d 6895 |
. . . . . 6
β’ (dom
(iEdgβπΊ) = β
β (β―β{π₯
β dom (iEdgβπΊ)
β£ π β
((iEdgβπΊ)βπ₯)}) =
(β―ββ
)) |
| 21 | | hash0 14331 |
. . . . . 6
β’
(β―ββ
) = 0 |
| 22 | 20, 21 | eqtrdi 2788 |
. . . . 5
β’ (dom
(iEdgβπΊ) = β
β (β―β{π₯
β dom (iEdgβπΊ)
β£ π β
((iEdgβπΊ)βπ₯)}) = 0) |
| 23 | | rabeq 3446 |
. . . . . . 7
β’ (dom
(iEdgβπΊ) = β
β {π₯ β dom
(iEdgβπΊ) β£
((iEdgβπΊ)βπ₯) = {π}} = {π₯ β β
β£ ((iEdgβπΊ)βπ₯) = {π}}) |
| 24 | 23 | fveq2d 6895 |
. . . . . 6
β’ (dom
(iEdgβπΊ) = β
β (β―β{π₯
β dom (iEdgβπΊ)
β£ ((iEdgβπΊ)βπ₯) = {π}}) = (β―β{π₯ β β
β£ ((iEdgβπΊ)βπ₯) = {π}})) |
| 25 | | rab0 4382 |
. . . . . . . 8
β’ {π₯ β β
β£
((iEdgβπΊ)βπ₯) = {π}} = β
|
| 26 | 25 | fveq2i 6894 |
. . . . . . 7
β’
(β―β{π₯
β β
β£ ((iEdgβπΊ)βπ₯) = {π}}) =
(β―ββ
) |
| 27 | 26, 21 | eqtri 2760 |
. . . . . 6
β’
(β―β{π₯
β β
β£ ((iEdgβπΊ)βπ₯) = {π}}) = 0 |
| 28 | 24, 27 | eqtrdi 2788 |
. . . . 5
β’ (dom
(iEdgβπΊ) = β
β (β―β{π₯
β dom (iEdgβπΊ)
β£ ((iEdgβπΊ)βπ₯) = {π}}) = 0) |
| 29 | 22, 28 | oveq12d 7429 |
. . . 4
β’ (dom
(iEdgβπΊ) = β
β ((β―β{π₯
β dom (iEdgβπΊ)
β£ π β
((iEdgβπΊ)βπ₯)}) + (β―β{π₯ β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ₯) = {π}})) = (0 + 0)) |
| 30 | 16, 29 | syl 17 |
. . 3
β’ ((π β π β§ πΌ = β
) β ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) + (β―β{π₯ β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ₯) = {π}})) = (0 + 0)) |
| 31 | | 00id 11393 |
. . 3
β’ (0 + 0) =
0 |
| 32 | 30, 31 | eqtrdi 2788 |
. 2
β’ ((π β π β§ πΌ = β
) β ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) + (β―β{π₯ β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ₯) = {π}})) = 0) |
| 33 | 14, 32 | eqtrd 2772 |
1
β’ ((π β π β§ πΌ = β
) β ((VtxDegβπΊ)βπ) = 0) |
