Step |
Hyp |
Ref |
Expression |
1 |
|
finsumvtxdg2sstep.v |
|- V = ( Vtx ` G ) |
2 |
|
finsumvtxdg2sstep.e |
|- E = ( iEdg ` G ) |
3 |
|
finsumvtxdg2sstep.k |
|- K = ( V \ { N } ) |
4 |
|
finsumvtxdg2sstep.i |
|- I = { i e. dom E | N e/ ( E ` i ) } |
5 |
|
finsumvtxdg2sstep.p |
|- P = ( E |` I ) |
6 |
|
finsumvtxdg2sstep.s |
|- S = <. K , P >. |
7 |
|
finsumvtxdg2ssteplem.j |
|- J = { i e. dom E | N e. ( E ` i ) } |
8 |
|
dmfi |
|- ( E e. Fin -> dom E e. Fin ) |
9 |
8
|
adantl |
|- ( ( V e. Fin /\ E e. Fin ) -> dom E e. Fin ) |
10 |
|
simpr |
|- ( ( G e. UPGraph /\ N e. V ) -> N e. V ) |
11 |
|
eqid |
|- dom E = dom E |
12 |
1 2 11
|
vtxdgfival |
|- ( ( dom E e. Fin /\ N e. V ) -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { i e. dom E | N e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) |
13 |
9 10 12
|
syl2anr |
|- ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { i e. dom E | N e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) |
14 |
7
|
eqcomi |
|- { i e. dom E | N e. ( E ` i ) } = J |
15 |
14
|
fveq2i |
|- ( # ` { i e. dom E | N e. ( E ` i ) } ) = ( # ` J ) |
16 |
15
|
a1i |
|- ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` { i e. dom E | N e. ( E ` i ) } ) = ( # ` J ) ) |
17 |
16
|
oveq1d |
|- ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( # ` { i e. dom E | N e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) |
18 |
13 17
|
eqtrd |
|- ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) |