Step | Hyp | Ref
| Expression |
1 | | df-vtxdg 28463 |
. 2
β’ VtxDeg =
(π β V β¦
β¦(Vtxβπ) / π£β¦β¦(iEdgβπ) / πβ¦(π’ β π£ β¦ ((β―β{π₯ β dom π β£ π’ β (πβπ₯)}) +π (β―β{π₯ β dom π β£ (πβπ₯) = {π’}})))) |
2 | | fvex 6859 |
. . . 4
β’
(Vtxβπ) β
V |
3 | | fvex 6859 |
. . . 4
β’
(iEdgβπ)
β V |
4 | | simpl 484 |
. . . . 5
β’ ((π£ = (Vtxβπ) β§ π = (iEdgβπ)) β π£ = (Vtxβπ)) |
5 | | dmeq 5863 |
. . . . . . . . 9
β’ (π = (iEdgβπ) β dom π = dom (iEdgβπ)) |
6 | | fveq1 6845 |
. . . . . . . . . 10
β’ (π = (iEdgβπ) β (πβπ₯) = ((iEdgβπ)βπ₯)) |
7 | 6 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = (iEdgβπ) β (π’ β (πβπ₯) β π’ β ((iEdgβπ)βπ₯))) |
8 | 5, 7 | rabeqbidv 3423 |
. . . . . . . 8
β’ (π = (iEdgβπ) β {π₯ β dom π β£ π’ β (πβπ₯)} = {π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) |
9 | 8 | fveq2d 6850 |
. . . . . . 7
β’ (π = (iEdgβπ) β (β―β{π₯ β dom π β£ π’ β (πβπ₯)}) = (β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)})) |
10 | 6 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π = (iEdgβπ) β ((πβπ₯) = {π’} β ((iEdgβπ)βπ₯) = {π’})) |
11 | 5, 10 | rabeqbidv 3423 |
. . . . . . . 8
β’ (π = (iEdgβπ) β {π₯ β dom π β£ (πβπ₯) = {π’}} = {π₯ β dom (iEdgβπ) β£ ((iEdgβπ)βπ₯) = {π’}}) |
12 | 11 | fveq2d 6850 |
. . . . . . 7
β’ (π = (iEdgβπ) β (β―β{π₯ β dom π β£ (πβπ₯) = {π’}}) = (β―β{π₯ β dom (iEdgβπ) β£ ((iEdgβπ)βπ₯) = {π’}})) |
13 | 9, 12 | oveq12d 7379 |
. . . . . 6
β’ (π = (iEdgβπ) β ((β―β{π₯ β dom π β£ π’ β (πβπ₯)}) +π
(β―β{π₯ β
dom π β£ (πβπ₯) = {π’}})) = ((β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) +π
(β―β{π₯ β
dom (iEdgβπ) β£
((iEdgβπ)βπ₯) = {π’}}))) |
14 | 13 | adantl 483 |
. . . . 5
β’ ((π£ = (Vtxβπ) β§ π = (iEdgβπ)) β ((β―β{π₯ β dom π β£ π’ β (πβπ₯)}) +π
(β―β{π₯ β
dom π β£ (πβπ₯) = {π’}})) = ((β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) +π
(β―β{π₯ β
dom (iEdgβπ) β£
((iEdgβπ)βπ₯) = {π’}}))) |
15 | 4, 14 | mpteq12dv 5200 |
. . . 4
β’ ((π£ = (Vtxβπ) β§ π = (iEdgβπ)) β (π’ β π£ β¦ ((β―β{π₯ β dom π β£ π’ β (πβπ₯)}) +π
(β―β{π₯ β
dom π β£ (πβπ₯) = {π’}}))) = (π’ β (Vtxβπ) β¦ ((β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) +π
(β―β{π₯ β
dom (iEdgβπ) β£
((iEdgβπ)βπ₯) = {π’}})))) |
16 | 2, 3, 15 | csbie2 3901 |
. . 3
β’
β¦(Vtxβπ) / π£β¦β¦(iEdgβπ) / πβ¦(π’ β π£ β¦ ((β―β{π₯ β dom π β£ π’ β (πβπ₯)}) +π (β―β{π₯ β dom π β£ (πβπ₯) = {π’}}))) = (π’ β (Vtxβπ) β¦ ((β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) +π (β―β{π₯ β dom (iEdgβπ) β£ ((iEdgβπ)βπ₯) = {π’}}))) |
17 | | fveq2 6846 |
. . . . . 6
β’ (π = πΊ β (Vtxβπ) = (VtxβπΊ)) |
18 | | vtxdgfval.v |
. . . . . 6
β’ π = (VtxβπΊ) |
19 | 17, 18 | eqtr4di 2791 |
. . . . 5
β’ (π = πΊ β (Vtxβπ) = π) |
20 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = πΊ β (iEdgβπ) = (iEdgβπΊ)) |
21 | 20 | dmeqd 5865 |
. . . . . . . . 9
β’ (π = πΊ β dom (iEdgβπ) = dom (iEdgβπΊ)) |
22 | | vtxdgfval.a |
. . . . . . . . . 10
β’ π΄ = dom πΌ |
23 | | vtxdgfval.i |
. . . . . . . . . . 11
β’ πΌ = (iEdgβπΊ) |
24 | 23 | dmeqi 5864 |
. . . . . . . . . 10
β’ dom πΌ = dom (iEdgβπΊ) |
25 | 22, 24 | eqtri 2761 |
. . . . . . . . 9
β’ π΄ = dom (iEdgβπΊ) |
26 | 21, 25 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΊ β dom (iEdgβπ) = π΄) |
27 | 20, 23 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π = πΊ β (iEdgβπ) = πΌ) |
28 | 27 | fveq1d 6848 |
. . . . . . . . 9
β’ (π = πΊ β ((iEdgβπ)βπ₯) = (πΌβπ₯)) |
29 | 28 | eleq2d 2820 |
. . . . . . . 8
β’ (π = πΊ β (π’ β ((iEdgβπ)βπ₯) β π’ β (πΌβπ₯))) |
30 | 26, 29 | rabeqbidv 3423 |
. . . . . . 7
β’ (π = πΊ β {π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)} = {π₯ β π΄ β£ π’ β (πΌβπ₯)}) |
31 | 30 | fveq2d 6850 |
. . . . . 6
β’ (π = πΊ β (β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) = (β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)})) |
32 | 28 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = πΊ β (((iEdgβπ)βπ₯) = {π’} β (πΌβπ₯) = {π’})) |
33 | 26, 32 | rabeqbidv 3423 |
. . . . . . 7
β’ (π = πΊ β {π₯ β dom (iEdgβπ) β£ ((iEdgβπ)βπ₯) = {π’}} = {π₯ β π΄ β£ (πΌβπ₯) = {π’}}) |
34 | 33 | fveq2d 6850 |
. . . . . 6
β’ (π = πΊ β (β―β{π₯ β dom (iEdgβπ) β£ ((iEdgβπ)βπ₯) = {π’}}) = (β―β{π₯ β π΄ β£ (πΌβπ₯) = {π’}})) |
35 | 31, 34 | oveq12d 7379 |
. . . . 5
β’ (π = πΊ β ((β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) +π
(β―β{π₯ β
dom (iEdgβπ) β£
((iEdgβπ)βπ₯) = {π’}})) = ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}}))) |
36 | 19, 35 | mpteq12dv 5200 |
. . . 4
β’ (π = πΊ β (π’ β (Vtxβπ) β¦ ((β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) +π
(β―β{π₯ β
dom (iEdgβπ) β£
((iEdgβπ)βπ₯) = {π’}}))) = (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}})))) |
37 | 36 | adantl 483 |
. . 3
β’ ((πΊ β π β§ π = πΊ) β (π’ β (Vtxβπ) β¦ ((β―β{π₯ β dom (iEdgβπ) β£ π’ β ((iEdgβπ)βπ₯)}) +π
(β―β{π₯ β
dom (iEdgβπ) β£
((iEdgβπ)βπ₯) = {π’}}))) = (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}})))) |
38 | 16, 37 | eqtrid 2785 |
. 2
β’ ((πΊ β π β§ π = πΊ) β β¦(Vtxβπ) / π£β¦β¦(iEdgβπ) / πβ¦(π’ β π£ β¦ ((β―β{π₯ β dom π β£ π’ β (πβπ₯)}) +π (β―β{π₯ β dom π β£ (πβπ₯) = {π’}}))) = (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π (β―β{π₯ β π΄ β£ (πΌβπ₯) = {π’}})))) |
39 | | elex 3465 |
. 2
β’ (πΊ β π β πΊ β V) |
40 | 18 | fvexi 6860 |
. . 3
β’ π β V |
41 | | mptexg 7175 |
. . 3
β’ (π β V β (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}}))) β V) |
42 | 40, 41 | mp1i 13 |
. 2
β’ (πΊ β π β (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}}))) β V) |
43 | 1, 38, 39, 42 | fvmptd2 6960 |
1
β’ (πΊ β π β (VtxDegβπΊ) = (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π
(β―β{π₯ β
π΄ β£ (πΌβπ₯) = {π’}})))) |