Step | Hyp | Ref
| Expression |
1 | | vtxdushgrfvedg.d |
. . . 4
β’ π· = (VtxDegβπΊ) |
2 | 1 | fveq1i 6893 |
. . 3
β’ (π·βπ) = ((VtxDegβπΊ)βπ) |
3 | 2 | a1i 11 |
. 2
β’ ((πΊ β USHGraph β§ π β π) β (π·βπ) = ((VtxDegβπΊ)βπ)) |
4 | | vtxdushgrfvedg.v |
. . . 4
β’ π = (VtxβπΊ) |
5 | | eqid 2731 |
. . . 4
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
6 | | eqid 2731 |
. . . 4
β’ dom
(iEdgβπΊ) = dom
(iEdgβπΊ) |
7 | 4, 5, 6 | vtxdgval 28989 |
. . 3
β’ (π β π β ((VtxDegβπΊ)βπ) = ((β―β{π β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ)}) +π
(β―β{π β
dom (iEdgβπΊ) β£
((iEdgβπΊ)βπ) = {π}}))) |
8 | 7 | adantl 481 |
. 2
β’ ((πΊ β USHGraph β§ π β π) β ((VtxDegβπΊ)βπ) = ((β―β{π β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ)}) +π
(β―β{π β
dom (iEdgβπΊ) β£
((iEdgβπΊ)βπ) = {π}}))) |
9 | | vtxdushgrfvedg.e |
. . . 4
β’ πΈ = (EdgβπΊ) |
10 | 4, 9 | vtxdushgrfvedglem 29010 |
. . 3
β’ ((πΊ β USHGraph β§ π β π) β (β―β{π β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ)}) = (β―β{π β πΈ β£ π β π})) |
11 | | fvex 6905 |
. . . . . . 7
β’
(iEdgβπΊ)
β V |
12 | 11 | dmex 7905 |
. . . . . 6
β’ dom
(iEdgβπΊ) β
V |
13 | 12 | rabex 5333 |
. . . . 5
β’ {π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}} β V |
14 | 13 | a1i 11 |
. . . 4
β’ ((πΊ β USHGraph β§ π β π) β {π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}} β V) |
15 | | eqid 2731 |
. . . . 5
β’ {π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}} = {π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}} |
16 | | eqeq1 2735 |
. . . . . 6
β’ (π = π β (π = {π} β π = {π})) |
17 | 16 | cbvrabv 3441 |
. . . . 5
β’ {π β πΈ β£ π = {π}} = {π β πΈ β£ π = {π}} |
18 | | eqid 2731 |
. . . . 5
β’ (π₯ β {π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}} β¦ ((iEdgβπΊ)βπ₯)) = (π₯ β {π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}} β¦ ((iEdgβπΊ)βπ₯)) |
19 | 9, 5, 15, 17, 18 | ushgredgedgloop 28752 |
. . . 4
β’ ((πΊ β USHGraph β§ π β π) β (π₯ β {π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}} β¦ ((iEdgβπΊ)βπ₯)):{π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}}β1-1-ontoβ{π β πΈ β£ π = {π}}) |
20 | 14, 19 | hasheqf1od 14318 |
. . 3
β’ ((πΊ β USHGraph β§ π β π) β (β―β{π β dom (iEdgβπΊ) β£ ((iEdgβπΊ)βπ) = {π}}) = (β―β{π β πΈ β£ π = {π}})) |
21 | 10, 20 | oveq12d 7430 |
. 2
β’ ((πΊ β USHGraph β§ π β π) β ((β―β{π β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ)}) +π
(β―β{π β
dom (iEdgβπΊ) β£
((iEdgβπΊ)βπ) = {π}})) = ((β―β{π β πΈ β£ π β π}) +π
(β―β{π β
πΈ β£ π = {π}}))) |
22 | 3, 8, 21 | 3eqtrd 2775 |
1
β’ ((πΊ β USHGraph β§ π β π) β (π·βπ) = ((β―β{π β πΈ β£ π β π}) +π
(β―β{π β
πΈ β£ π = {π}}))) |