Metamath Proof Explorer


Theorem vtxdgfval

Description: The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 9-Dec-2020)

Ref Expression
Hypotheses vtxdgfval.v V = Vtx G
vtxdgfval.i I = iEdg G
vtxdgfval.a A = dom I
Assertion vtxdgfval G W VtxDeg G = u V x A | u I x + 𝑒 x A | I x = u

Proof

Step Hyp Ref Expression
1 vtxdgfval.v V = Vtx G
2 vtxdgfval.i I = iEdg G
3 vtxdgfval.a A = dom I
4 df-vtxdg VtxDeg = g V Vtx g / v iEdg g / e u v x dom e | u e x + 𝑒 x dom e | e x = u
5 fvex Vtx g V
6 fvex iEdg g V
7 simpl v = Vtx g e = iEdg g v = Vtx g
8 dmeq e = iEdg g dom e = dom iEdg g
9 fveq1 e = iEdg g e x = iEdg g x
10 9 eleq2d e = iEdg g u e x u iEdg g x
11 8 10 rabeqbidv e = iEdg g x dom e | u e x = x dom iEdg g | u iEdg g x
12 11 fveq2d e = iEdg g x dom e | u e x = x dom iEdg g | u iEdg g x
13 9 eqeq1d e = iEdg g e x = u iEdg g x = u
14 8 13 rabeqbidv e = iEdg g x dom e | e x = u = x dom iEdg g | iEdg g x = u
15 14 fveq2d e = iEdg g x dom e | e x = u = x dom iEdg g | iEdg g x = u
16 12 15 oveq12d e = iEdg g x dom e | u e x + 𝑒 x dom e | e x = u = x dom iEdg g | u iEdg g x + 𝑒 x dom iEdg g | iEdg g x = u
17 16 adantl v = Vtx g e = iEdg g x dom e | u e x + 𝑒 x dom e | e x = u = x dom iEdg g | u iEdg g x + 𝑒 x dom iEdg g | iEdg g x = u
18 7 17 mpteq12dv v = Vtx g e = iEdg g u v x dom e | u e x + 𝑒 x dom e | e x = u = u Vtx g x dom iEdg g | u iEdg g x + 𝑒 x dom iEdg g | iEdg g x = u
19 5 6 18 csbie2 Vtx g / v iEdg g / e u v x dom e | u e x + 𝑒 x dom e | e x = u = u Vtx g x dom iEdg g | u iEdg g x + 𝑒 x dom iEdg g | iEdg g x = u
20 fveq2 g = G Vtx g = Vtx G
21 20 1 eqtr4di g = G Vtx g = V
22 fveq2 g = G iEdg g = iEdg G
23 22 dmeqd g = G dom iEdg g = dom iEdg G
24 2 dmeqi dom I = dom iEdg G
25 3 24 eqtri A = dom iEdg G
26 23 25 eqtr4di g = G dom iEdg g = A
27 22 2 eqtr4di g = G iEdg g = I
28 27 fveq1d g = G iEdg g x = I x
29 28 eleq2d g = G u iEdg g x u I x
30 26 29 rabeqbidv g = G x dom iEdg g | u iEdg g x = x A | u I x
31 30 fveq2d g = G x dom iEdg g | u iEdg g x = x A | u I x
32 28 eqeq1d g = G iEdg g x = u I x = u
33 26 32 rabeqbidv g = G x dom iEdg g | iEdg g x = u = x A | I x = u
34 33 fveq2d g = G x dom iEdg g | iEdg g x = u = x A | I x = u
35 31 34 oveq12d g = G x dom iEdg g | u iEdg g x + 𝑒 x dom iEdg g | iEdg g x = u = x A | u I x + 𝑒 x A | I x = u
36 21 35 mpteq12dv g = G u Vtx g x dom iEdg g | u iEdg g x + 𝑒 x dom iEdg g | iEdg g x = u = u V x A | u I x + 𝑒 x A | I x = u
37 36 adantl G W g = G u Vtx g x dom iEdg g | u iEdg g x + 𝑒 x dom iEdg g | iEdg g x = u = u V x A | u I x + 𝑒 x A | I x = u
38 19 37 syl5eq G W g = G Vtx g / v iEdg g / e u v x dom e | u e x + 𝑒 x dom e | e x = u = u V x A | u I x + 𝑒 x A | I x = u
39 elex G W G V
40 1 fvexi V V
41 mptexg V V u V x A | u I x + 𝑒 x A | I x = u V
42 40 41 mp1i G W u V x A | u I x + 𝑒 x A | I x = u V
43 4 38 39 42 fvmptd2 G W VtxDeg G = u V x A | u I x + 𝑒 x A | I x = u