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	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	vtxduhgrun.j	⊢ 𝐽 = ( iEdg ‘ 𝐻 )
	vtxduhgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxduhgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
	vtxduhgrun.vu	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
	vtxduhgrun.d	⊢ ( 𝜑 → ( dom 𝐼 ∩ dom 𝐽 ) = ∅ )
	vtxduhgrun.g	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
	vtxduhgrun.h	⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
	vtxduhgrun.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
	vtxduhgrun.u	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐼 ∪ 𝐽 ) )
Assertion	vtxduhgrun	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝑈 ) ‘ 𝑁 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) +𝑒 ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		vtxduhgrun.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		vtxduhgrun.j	⊢ 𝐽 = ( iEdg ‘ 𝐻 )
3		vtxduhgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		vtxduhgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
5		vtxduhgrun.vu	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
6		vtxduhgrun.d	⊢ ( 𝜑 → ( dom 𝐼 ∩ dom 𝐽 ) = ∅ )
7		vtxduhgrun.g	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
8		vtxduhgrun.h	⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
9		vtxduhgrun.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
10		vtxduhgrun.u	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐼 ∪ 𝐽 ) )
11	1	uhgrfun	⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
12	7 11	syl	⊢ ( 𝜑 → Fun 𝐼 )
13	2	uhgrfun	⊢ ( 𝐻 ∈ UHGraph → Fun 𝐽 )
14	8 13	syl	⊢ ( 𝜑 → Fun 𝐽 )
15	1 2 3 4 5 6 12 14 9 10	vtxdun	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝑈 ) ‘ 𝑁 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) +𝑒 ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ) )