Step | Hyp | Ref
| Expression |
1 | | vtxdgval.v |
. . . . 5
β’ π = (VtxβπΊ) |
2 | 1 | 1vgrex 27995 |
. . . 4
β’ (π β π β πΊ β V) |
3 | | vtxdgval.i |
. . . . 5
β’ πΌ = (iEdgβπΊ) |
4 | | vtxdgval.a |
. . . . 5
β’ π΄ = dom πΌ |
5 | 1, 3, 4 | vtxdgfval 28457 |
. . . 4
β’ (πΊ β V β
(VtxDegβπΊ) = (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}})))) |
6 | 2, 5 | syl 17 |
. . 3
β’ (π β π β (VtxDegβπΊ) = (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}})))) |
7 | 6 | fveq1d 6849 |
. 2
β’ (π β π β ((VtxDegβπΊ)βπ) = ((π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}})))βπ)) |
8 | | eleq1 2826 |
. . . . . 6
β’ (π’ = π β (π’ β (πΌβπ₯) β π β (πΌβπ₯))) |
9 | 8 | rabbidv 3418 |
. . . . 5
β’ (π’ = π β {π₯ β π΄ β£ π’ β (πΌβπ₯)} = {π₯ β π΄ β£ π β (πΌβπ₯)}) |
10 | 9 | fveq2d 6851 |
. . . 4
β’ (π’ = π β (β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) = (β―β{π₯ β π΄ β£ π β (πΌβπ₯)})) |
11 | | sneq 4601 |
. . . . . . 7
β’ (π’ = π β {π’} = {π}) |
12 | 11 | eqeq2d 2748 |
. . . . . 6
β’ (π’ = π β ((πΌβπ₯) = {π’} β (πΌβπ₯) = {π})) |
13 | 12 | rabbidv 3418 |
. . . . 5
β’ (π’ = π β {π₯ β π΄ β£ (πΌβπ₯) = {π’}} = {π₯ β π΄ β£ (πΌβπ₯) = {π}}) |
14 | 13 | fveq2d 6851 |
. . . 4
β’ (π’ = π β (β―β{π₯ β π΄ β£ (πΌβπ₯) = {π’}}) = (β―β{π₯ β π΄ β£ (πΌβπ₯) = {π}})) |
15 | 10, 14 | oveq12d 7380 |
. . 3
β’ (π’ = π β ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}})) = ((β―β{π₯ β π΄ β£ π β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π}}))) |
16 | | eqid 2737 |
. . 3
β’ (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}}))) = (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}}))) |
17 | | ovex 7395 |
. . 3
β’
((β―β{π₯
β π΄ β£ π β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π}})) β V |
18 | 15, 16, 17 | fvmpt 6953 |
. 2
β’ (π β π β ((π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}})))βπ) = ((β―β{π₯ β π΄ β£ π β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π}}))) |
19 | 7, 18 | eqtrd 2777 |
1
β’ (π β π β ((VtxDegβπΊ)βπ) = ((β―β{π₯ β π΄ β£ π β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π}}))) |