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

Definition df-vdgr 23736
Description: Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, we have to double-count those edges that contain  u "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  +e 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  e.  _V , 
e  e.  _V  |->  ( u  e.  v  |->  ( ( # `  {
x  e.  dom  e  |  u  e.  (
e `  x ) } ) +e
( # `  { x  e.  dom  e  |  ( e `  x )  =  { u } } ) ) ) )
Distinct variable group:    u, e, v, x

Detailed syntax breakdown of Definition df-vdgr
StepHypRef Expression
1 cvdg 23735 . 2  class VDeg
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 3078 . . 3  class  _V
5 vu . . . 4  setvar  u
62cv 1369 . . . 4  class  v
75cv 1369 . . . . . . . 8  class  u
8 vx . . . . . . . . . 10  setvar  x
98cv 1369 . . . . . . . . 9  class  x
103cv 1369 . . . . . . . . 9  class  e
119, 10cfv 5529 . . . . . . . 8  class  ( e `
 x )
127, 11wcel 1758 . . . . . . 7  wff  u  e.  ( e `  x
)
1310cdm 4951 . . . . . . 7  class  dom  e
1412, 8, 13crab 2803 . . . . . 6  class  { x  e.  dom  e  |  u  e.  ( e `  x ) }
15 chash 12223 . . . . . 6  class  #
1614, 15cfv 5529 . . . . 5  class  ( # `  { x  e.  dom  e  |  u  e.  ( e `  x
) } )
177csn 3988 . . . . . . . 8  class  { u }
1811, 17wceq 1370 . . . . . . 7  wff  ( e `
 x )  =  { u }
1918, 8, 13crab 2803 . . . . . 6  class  { x  e.  dom  e  |  ( e `  x )  =  { u } }
2019, 15cfv 5529 . . . . 5  class  ( # `  { x  e.  dom  e  |  ( e `  x )  =  {
u } } )
21 cxad 11201 . . . . 5  class  +e
2216, 20, 21co 6203 . . . 4  class  ( (
# `  { x  e.  dom  e  |  u  e.  ( e `  x ) } ) +e ( # `  { x  e.  dom  e  |  ( e `  x )  =  {
u } } ) )
235, 6, 22cmpt 4461 . . 3  class  ( u  e.  v  |->  ( (
# `  { x  e.  dom  e  |  u  e.  ( e `  x ) } ) +e ( # `  { x  e.  dom  e  |  ( e `  x )  =  {
u } } ) ) )
242, 3, 4, 4, 23cmpt2 6205 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  ( u  e.  v  |->  ( (
# `  { x  e.  dom  e  |  u  e.  ( e `  x ) } ) +e ( # `  { x  e.  dom  e  |  ( e `  x )  =  {
u } } ) ) ) )
251, 24wceq 1370 1  wff VDeg  =  ( v  e.  _V , 
e  e.  _V  |->  ( u  e.  v  |->  ( ( # `  {
x  e.  dom  e  |  u  e.  (
e `  x ) } ) +e
( # `  { x  e.  dom  e  |  ( e `  x )  =  { u } } ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  vdgrfval  23737
  Copyright terms: Public domain W3C validator