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 = ( iEdg ` G ) |
|
| vtxduhgrun.j | |- J = ( iEdg ` H ) |
||
| vtxduhgrun.vg | |- V = ( Vtx ` G ) |
||
| vtxduhgrun.vh | |- ( ph -> ( Vtx ` H ) = V ) |
||
| vtxduhgrun.vu | |- ( ph -> ( Vtx ` U ) = V ) |
||
| vtxduhgrun.d | |- ( ph -> ( dom I i^i dom J ) = (/) ) |
||
| vtxduhgrun.g | |- ( ph -> G e. UHGraph ) |
||
| vtxduhgrun.h | |- ( ph -> H e. UHGraph ) |
||
| vtxduhgrun.n | |- ( ph -> N e. V ) |
||
| vtxduhgrun.u | |- ( ph -> ( iEdg ` U ) = ( I u. J ) ) |
||
| Assertion | vtxduhgrun | |- ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtxduhgrun.i | |- I = ( iEdg ` G ) |
|
| 2 | vtxduhgrun.j | |- J = ( iEdg ` H ) |
|
| 3 | vtxduhgrun.vg | |- V = ( Vtx ` G ) |
|
| 4 | vtxduhgrun.vh | |- ( ph -> ( Vtx ` H ) = V ) |
|
| 5 | vtxduhgrun.vu | |- ( ph -> ( Vtx ` U ) = V ) |
|
| 6 | vtxduhgrun.d | |- ( ph -> ( dom I i^i dom J ) = (/) ) |
|
| 7 | vtxduhgrun.g | |- ( ph -> G e. UHGraph ) |
|
| 8 | vtxduhgrun.h | |- ( ph -> H e. UHGraph ) |
|
| 9 | vtxduhgrun.n | |- ( ph -> N e. V ) |
|
| 10 | vtxduhgrun.u | |- ( ph -> ( iEdg ` U ) = ( I u. J ) ) |
|
| 11 | 1 | uhgrfun | |- ( G e. UHGraph -> Fun I ) |
| 12 | 7 11 | syl | |- ( ph -> Fun I ) |
| 13 | 2 | uhgrfun | |- ( H e. UHGraph -> Fun J ) |
| 14 | 8 13 | syl | |- ( ph -> Fun J ) |
| 15 | 1 2 3 4 5 6 12 14 9 10 | vtxdun | |- ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) ) |