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=\mathrm{iEdg}\left(G\right)$$
	vtxduhgrun.j	$$⊢J=\mathrm{iEdg}\left(H\right)$$
	vtxduhgrun.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	vtxduhgrun.vh	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
	vtxduhgrun.vu	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
	vtxduhgrun.d	$$⊢\phi \to \mathrm{dom}I\cap \mathrm{dom}J=\varnothing$$
	vtxduhgrun.g	$$⊢\phi \to G\in \mathrm{UHGraph}$$
	vtxduhgrun.h	$$⊢\phi \to H\in \mathrm{UHGraph}$$
	vtxduhgrun.n	$$⊢\phi \to N\in V$$
	vtxduhgrun.u	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=I\cup J$$
Assertion	vtxduhgrun	$$⊢\phi \to \mathrm{VtxDeg}\left(U\right)\left(N\right)=\mathrm{VtxDeg}\left(G\right)\left(N\right){+}_{𝑒}\mathrm{VtxDeg}\left(H\right)\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		vtxduhgrun.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
2		vtxduhgrun.j	$$⊢J=\mathrm{iEdg}\left(H\right)$$
3		vtxduhgrun.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
4		vtxduhgrun.vh	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
5		vtxduhgrun.vu	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
6		vtxduhgrun.d	$$⊢\phi \to \mathrm{dom}I\cap \mathrm{dom}J=\varnothing$$
7		vtxduhgrun.g	$$⊢\phi \to G\in \mathrm{UHGraph}$$
8		vtxduhgrun.h	$$⊢\phi \to H\in \mathrm{UHGraph}$$
9		vtxduhgrun.n	$$⊢\phi \to N\in V$$
10		vtxduhgrun.u	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=I\cup J$$
11	1	uhgrfun	$$⊢G\in \mathrm{UHGraph}\to \mathrm{Fun}I$$
12	7 11	syl	$$⊢\phi \to \mathrm{Fun}I$$
13	2	uhgrfun	$$⊢H\in \mathrm{UHGraph}\to \mathrm{Fun}J$$
14	8 13	syl	$$⊢\phi \to \mathrm{Fun}J$$
15	1 2 3 4 5 6 12 14 9 10	vtxdun	$$⊢\phi \to \mathrm{VtxDeg}\left(U\right)\left(N\right)=\mathrm{VtxDeg}\left(G\right)\left(N\right){+}_{𝑒}\mathrm{VtxDeg}\left(H\right)\left(N\right)$$