Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vdgr Structured version   Visualization version   GIF version

Definition df-vdgr 26421
 Description: Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, we have to double-count those edges that contain 𝑢 "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +𝑒 is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)
Assertion
Ref Expression
df-vdgr VDeg = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
Distinct variable group:   𝑢,𝑒,𝑣,𝑥

Detailed syntax breakdown of Definition df-vdgr
StepHypRef Expression
1 cvdg 26420 . 2 class VDeg
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3173 . . 3 class V
5 vu . . . 4 setvar 𝑢
62cv 1474 . . . 4 class 𝑣
75cv 1474 . . . . . . . 8 class 𝑢
8 vx . . . . . . . . . 10 setvar 𝑥
98cv 1474 . . . . . . . . 9 class 𝑥
103cv 1474 . . . . . . . . 9 class 𝑒
119, 10cfv 5804 . . . . . . . 8 class (𝑒𝑥)
127, 11wcel 1977 . . . . . . 7 wff 𝑢 ∈ (𝑒𝑥)
1310cdm 5038 . . . . . . 7 class dom 𝑒
1412, 8, 13crab 2900 . . . . . 6 class {𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}
15 chash 12979 . . . . . 6 class #
1614, 15cfv 5804 . . . . 5 class (#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)})
177csn 4125 . . . . . . . 8 class {𝑢}
1811, 17wceq 1475 . . . . . . 7 wff (𝑒𝑥) = {𝑢}
1918, 8, 13crab 2900 . . . . . 6 class {𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}
2019, 15cfv 5804 . . . . 5 class (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})
21 cxad 11820 . . . . 5 class +𝑒
2216, 20, 21co 6549 . . . 4 class ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))
235, 6, 22cmpt 4643 . . 3 class (𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
242, 3, 4, 4, 23cmpt2 6551 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
251, 24wceq 1475 1 wff VDeg = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
 Colors of variables: wff setvar class This definition is referenced by:  vdgrfval  26422
 Copyright terms: Public domain W3C validator