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