Metamath Proof Explorer


Theorem vtxduhgrun

Description: The degree of a vertex in the union of two hypergraphs on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 21-Dec-2017) (Revised by AV, 12-Dec-2020) (Proof shortened by AV, 19-Feb-2021)

Ref Expression
Hypotheses vtxduhgrun.i I = iEdg G
vtxduhgrun.j J = iEdg H
vtxduhgrun.vg V = Vtx G
vtxduhgrun.vh φ Vtx H = V
vtxduhgrun.vu φ Vtx U = V
vtxduhgrun.d φ dom I dom J =
vtxduhgrun.g φ G UHGraph
vtxduhgrun.h φ H UHGraph
vtxduhgrun.n φ N V
vtxduhgrun.u φ iEdg U = I J
Assertion vtxduhgrun φ VtxDeg U N = VtxDeg G N + 𝑒 VtxDeg H N

Proof

Step Hyp Ref Expression
1 vtxduhgrun.i I = iEdg G
2 vtxduhgrun.j J = iEdg H
3 vtxduhgrun.vg V = Vtx G
4 vtxduhgrun.vh φ Vtx H = V
5 vtxduhgrun.vu φ Vtx U = V
6 vtxduhgrun.d φ dom I dom J =
7 vtxduhgrun.g φ G UHGraph
8 vtxduhgrun.h φ H UHGraph
9 vtxduhgrun.n φ N V
10 vtxduhgrun.u φ iEdg U = I J
11 1 uhgrfun G UHGraph Fun I
12 7 11 syl φ Fun I
13 2 uhgrfun H UHGraph Fun J
14 8 13 syl φ Fun J
15 1 2 3 4 5 6 12 14 9 10 vtxdun φ VtxDeg U N = VtxDeg G N + 𝑒 VtxDeg H N