Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdun.i |
|- I = ( iEdg ` G ) |
2 |
|
vtxdun.j |
|- J = ( iEdg ` H ) |
3 |
|
vtxdun.vg |
|- V = ( Vtx ` G ) |
4 |
|
vtxdun.vh |
|- ( ph -> ( Vtx ` H ) = V ) |
5 |
|
vtxdun.vu |
|- ( ph -> ( Vtx ` U ) = V ) |
6 |
|
vtxdun.d |
|- ( ph -> ( dom I i^i dom J ) = (/) ) |
7 |
|
vtxdun.fi |
|- ( ph -> Fun I ) |
8 |
|
vtxdun.fj |
|- ( ph -> Fun J ) |
9 |
|
vtxdun.n |
|- ( ph -> N e. V ) |
10 |
|
vtxdun.u |
|- ( ph -> ( iEdg ` U ) = ( I u. J ) ) |
11 |
|
vtxdfiun.a |
|- ( ph -> dom I e. Fin ) |
12 |
|
vtxdfiun.b |
|- ( ph -> dom J e. Fin ) |
13 |
1 2 3 4 5 6 7 8 9 10
|
vtxdun |
|- ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) ) |
14 |
|
eqid |
|- dom I = dom I |
15 |
3 1 14
|
vtxdgfisnn0 |
|- ( ( dom I e. Fin /\ N e. V ) -> ( ( VtxDeg ` G ) ` N ) e. NN0 ) |
16 |
11 9 15
|
syl2anc |
|- ( ph -> ( ( VtxDeg ` G ) ` N ) e. NN0 ) |
17 |
16
|
nn0red |
|- ( ph -> ( ( VtxDeg ` G ) ` N ) e. RR ) |
18 |
9 4
|
eleqtrrd |
|- ( ph -> N e. ( Vtx ` H ) ) |
19 |
|
eqid |
|- ( Vtx ` H ) = ( Vtx ` H ) |
20 |
|
eqid |
|- dom J = dom J |
21 |
19 2 20
|
vtxdgfisnn0 |
|- ( ( dom J e. Fin /\ N e. ( Vtx ` H ) ) -> ( ( VtxDeg ` H ) ` N ) e. NN0 ) |
22 |
12 18 21
|
syl2anc |
|- ( ph -> ( ( VtxDeg ` H ) ` N ) e. NN0 ) |
23 |
22
|
nn0red |
|- ( ph -> ( ( VtxDeg ` H ) ` N ) e. RR ) |
24 |
17 23
|
rexaddd |
|- ( ph -> ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) = ( ( ( VtxDeg ` G ) ` N ) + ( ( VtxDeg ` H ) ` N ) ) ) |
25 |
13 24
|
eqtrd |
|- ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( ( VtxDeg ` G ) ` N ) + ( ( VtxDeg ` H ) ` N ) ) ) |