This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-vtxdg

Description: Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, 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) (Revised by AV, 9-Dec-2020)

Ref Expression
Assertion df-vtxdg 
|- VtxDeg = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvtxdg 
 |-  VtxDeg
1 vg 
 |-  g
2 cvv 
 |-  _V
3 cvtx 
 |-  Vtx
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Vtx ` g )
6 vv 
 |-  v
7 ciedg 
 |-  iEdg
8 4 7 cfv 
 |-  ( iEdg ` g )
9 ve 
 |-  e
10 vu 
 |-  u
11 6 cv 
 |-  v
12 chash 
 |-  #
13 vx 
 |-  x
14 9 cv 
 |-  e
15 14 cdm 
 |-  dom e
16 10 cv 
 |-  u
17 13 cv 
 |-  x
18 17 14 cfv 
 |-  ( e ` x )
19 16 18 wcel 
 |-  u e. ( e ` x )
20 19 13 15 crab 
 |-  { x e. dom e | u e. ( e ` x ) }
21 20 12 cfv 
 |-  ( # ` { x e. dom e | u e. ( e ` x ) } )
22 cxad 
 |-  +e
23 16 csn 
 |-  { u }
24 18 23 wceq 
 |-  ( e ` x ) = { u }
25 24 13 15 crab 
 |-  { x e. dom e | ( e ` x ) = { u } }
26 25 12 cfv 
 |-  ( # ` { x e. dom e | ( e ` x ) = { u } } )
27 21 26 22 co 
 |-  ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) )
28 10 11 27 cmpt 
 |-  ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
29 9 8 28 csb 
 |-  [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
30 6 5 29 csb 
 |-  [_ ( Vtx ` g ) / v ]_ [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
31 1 2 30 cmpt 
 |-  ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )
32 0 31 wceq 
 |-  VtxDeg = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )