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 ‘ 𝐻 ) ‘ 𝑁 ) ) ) |