Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem3

Description: Lemma for finsumvtxdg2sstep . (Contributed by AV, 19-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 finsumvtxdg2ssteplem3 
|- ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( # ` J ) )

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 7 rabeq2i 
 |-  ( i e. J <-> ( i e. dom E /\ N e. ( E ` i ) ) )
9 8 anbi1i 
 |-  ( ( i e. J /\ v e. ( E ` i ) ) <-> ( ( i e. dom E /\ N e. ( E ` i ) ) /\ v e. ( E ` i ) ) )
10 anass 
 |-  ( ( ( i e. dom E /\ N e. ( E ` i ) ) /\ v e. ( E ` i ) ) <-> ( i e. dom E /\ ( N e. ( E ` i ) /\ v e. ( E ` i ) ) ) )
11 9 10 bitri 
 |-  ( ( i e. J /\ v e. ( E ` i ) ) <-> ( i e. dom E /\ ( N e. ( E ` i ) /\ v e. ( E ` i ) ) ) )
12 11 rabbia2 
 |-  { i e. J | v e. ( E ` i ) } = { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) }
13 12 fveq2i 
 |-  ( # ` { i e. J | v e. ( E ` i ) } ) = ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
14 13 a1i 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ v e. ( V \ { N } ) ) -> ( # ` { i e. J | v e. ( E ` i ) } ) = ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) )
15 14 sumeq2dv 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) = sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) )
16 15 oveq1d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) )
17 simpll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> G e. UPGraph )
18 simpr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( V e. Fin /\ E e. Fin ) )
19 simplr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> N e. V )
20 1 2 numedglnl 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( # ` { i e. dom E | N e. ( E ` i ) } ) )
21 17 18 19 20 syl3anc 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( # ` { i e. dom E | N e. ( E ` i ) } ) )
22 16 21 eqtrd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( # ` { i e. dom E | N e. ( E ` i ) } ) )
23 7 fveq2i 
 |-  ( # ` J ) = ( # ` { i e. dom E | N e. ( E ` i ) } )
24 22 23 eqtr4di 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( # ` J ) )