Metamath Proof Explorer


Theorem vtxdlfgrval

Description: The value of the vertex degree function for a loop-free graph G . (Contributed by AV, 23-Feb-2021)

Ref Expression
Hypotheses vtxdlfgrval.v V = Vtx G
vtxdlfgrval.i I = iEdg G
vtxdlfgrval.a A = dom I
vtxdlfgrval.d D = VtxDeg G
Assertion vtxdlfgrval I : A x 𝒫 V | 2 x U V D U = x A | U I x

Proof

Step Hyp Ref Expression
1 vtxdlfgrval.v V = Vtx G
2 vtxdlfgrval.i I = iEdg G
3 vtxdlfgrval.a A = dom I
4 vtxdlfgrval.d D = VtxDeg G
5 4 fveq1i D U = VtxDeg G U
6 1 2 3 vtxdgval U V VtxDeg G U = x A | U I x + 𝑒 x A | I x = U
7 6 adantl I : A x 𝒫 V | 2 x U V VtxDeg G U = x A | U I x + 𝑒 x A | I x = U
8 5 7 eqtrid I : A x 𝒫 V | 2 x U V D U = x A | U I x + 𝑒 x A | I x = U
9 eqid x 𝒫 V | 2 x = x 𝒫 V | 2 x
10 2 3 9 lfgrnloop I : A x 𝒫 V | 2 x x A | I x = U =
11 10 adantr I : A x 𝒫 V | 2 x U V x A | I x = U =
12 11 fveq2d I : A x 𝒫 V | 2 x U V x A | I x = U =
13 hash0 = 0
14 12 13 eqtrdi I : A x 𝒫 V | 2 x U V x A | I x = U = 0
15 14 oveq2d I : A x 𝒫 V | 2 x U V x A | U I x + 𝑒 x A | I x = U = x A | U I x + 𝑒 0
16 2 dmeqi dom I = dom iEdg G
17 3 16 eqtri A = dom iEdg G
18 fvex iEdg G V
19 18 dmex dom iEdg G V
20 17 19 eqeltri A V
21 20 rabex x A | U I x V
22 hashxnn0 x A | U I x V x A | U I x 0 *
23 xnn0xr x A | U I x 0 * x A | U I x *
24 21 22 23 mp2b x A | U I x *
25 xaddid1 x A | U I x * x A | U I x + 𝑒 0 = x A | U I x
26 24 25 mp1i I : A x 𝒫 V | 2 x U V x A | U I x + 𝑒 0 = x A | U I x
27 8 15 26 3eqtrd I : A x 𝒫 V | 2 x U V D U = x A | U I x