Metamath Proof Explorer


Theorem vtxdfiun

Description: The degree of a vertex in the union of two hypergraphs of finite size 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-Jan-2018) (Revised by AV, 19-Feb-2021)

Ref Expression
Hypotheses vtxdun.i 𝐼 = ( iEdg ‘ 𝐺 )
vtxdun.j 𝐽 = ( iEdg ‘ 𝐻 )
vtxdun.vg 𝑉 = ( Vtx ‘ 𝐺 )
vtxdun.vh ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
vtxdun.vu ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
vtxdun.d ( 𝜑 → ( dom 𝐼 ∩ dom 𝐽 ) = ∅ )
vtxdun.fi ( 𝜑 → Fun 𝐼 )
vtxdun.fj ( 𝜑 → Fun 𝐽 )
vtxdun.n ( 𝜑𝑁𝑉 )
vtxdun.u ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐼𝐽 ) )
vtxdfiun.a ( 𝜑 → dom 𝐼 ∈ Fin )
vtxdfiun.b ( 𝜑 → dom 𝐽 ∈ Fin )
Assertion vtxdfiun ( 𝜑 → ( ( VtxDeg ‘ 𝑈 ) ‘ 𝑁 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) + ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 vtxdun.i 𝐼 = ( iEdg ‘ 𝐺 )
2 vtxdun.j 𝐽 = ( iEdg ‘ 𝐻 )
3 vtxdun.vg 𝑉 = ( Vtx ‘ 𝐺 )
4 vtxdun.vh ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
5 vtxdun.vu ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
6 vtxdun.d ( 𝜑 → ( dom 𝐼 ∩ dom 𝐽 ) = ∅ )
7 vtxdun.fi ( 𝜑 → Fun 𝐼 )
8 vtxdun.fj ( 𝜑 → Fun 𝐽 )
9 vtxdun.n ( 𝜑𝑁𝑉 )
10 vtxdun.u ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐼𝐽 ) )
11 vtxdfiun.a ( 𝜑 → dom 𝐼 ∈ Fin )
12 vtxdfiun.b ( 𝜑 → dom 𝐽 ∈ Fin )
13 1 2 3 4 5 6 7 8 9 10 vtxdun ( 𝜑 → ( ( VtxDeg ‘ 𝑈 ) ‘ 𝑁 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) +𝑒 ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ) )
14 eqid dom 𝐼 = dom 𝐼
15 3 1 14 vtxdgfisnn0 ( ( dom 𝐼 ∈ Fin ∧ 𝑁𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ∈ ℕ0 )
16 11 9 15 syl2anc ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ∈ ℕ0 )
17 16 nn0red ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ∈ ℝ )
18 9 4 eleqtrrd ( 𝜑𝑁 ∈ ( Vtx ‘ 𝐻 ) )
19 eqid ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
20 eqid dom 𝐽 = dom 𝐽
21 19 2 20 vtxdgfisnn0 ( ( dom 𝐽 ∈ Fin ∧ 𝑁 ∈ ( Vtx ‘ 𝐻 ) ) → ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ∈ ℕ0 )
22 12 18 21 syl2anc ( 𝜑 → ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ∈ ℕ0 )
23 22 nn0red ( 𝜑 → ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ∈ ℝ )
24 17 23 rexaddd ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) +𝑒 ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) + ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ) )
25 13 24 eqtrd ( 𝜑 → ( ( VtxDeg ‘ 𝑈 ) ‘ 𝑁 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) + ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ) )