Metamath Proof Explorer


Theorem finsumvtxdg2ssteplem2

Description: Lemma for finsumvtxdg2sstep . (Contributed by AV, 12-Dec-2021)

Ref Expression
Hypotheses finsumvtxdg2sstep.v
|- V = ( Vtx ` G )
finsumvtxdg2sstep.e
|- E = ( iEdg ` G )
finsumvtxdg2sstep.k
|- K = ( V \ { N } )
finsumvtxdg2sstep.i
|- I = { i e. dom E | N e/ ( E ` i ) }
finsumvtxdg2sstep.p
|- P = ( E |` I )
finsumvtxdg2sstep.s
|- S = <. K , P >.
finsumvtxdg2ssteplem.j
|- J = { i e. dom E | N e. ( E ` i ) }
Assertion finsumvtxdg2ssteplem2
|- ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) )

Proof

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 } } ) ) )