Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem1

Description: Lemma for finsumvtxdg2sstep . (Contributed by AV, 15-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 finsumvtxdg2ssteplem1 
|- ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` E ) = ( ( # ` P ) + ( # ` 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 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
9 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun E )
10 8 9 syl 
 |-  ( G e. UPGraph -> Fun E )
11 10 ad2antrr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> Fun E )
12 simprr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> E e. Fin )
13 4 ssrab3 
 |-  I C_ dom E
14 13 a1i 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> I C_ dom E )
15 hashreshashfun 
 |-  ( ( Fun E /\ E e. Fin /\ I C_ dom E ) -> ( # ` E ) = ( ( # ` ( E |` I ) ) + ( # ` ( dom E \ I ) ) ) )
16 11 12 14 15 syl3anc 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` E ) = ( ( # ` ( E |` I ) ) + ( # ` ( dom E \ I ) ) ) )
17 5 eqcomi 
 |-  ( E |` I ) = P
18 17 fveq2i 
 |-  ( # ` ( E |` I ) ) = ( # ` P )
19 18 a1i 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` ( E |` I ) ) = ( # ` P ) )
20 notrab 
 |-  ( dom E \ { i e. dom E | N e/ ( E ` i ) } ) = { i e. dom E | -. N e/ ( E ` i ) }
21 4 difeq2i 
 |-  ( dom E \ I ) = ( dom E \ { i e. dom E | N e/ ( E ` i ) } )
22 nnel 
 |-  ( -. N e/ ( E ` i ) <-> N e. ( E ` i ) )
23 22 bicomi 
 |-  ( N e. ( E ` i ) <-> -. N e/ ( E ` i ) )
24 23 rabbii 
 |-  { i e. dom E | N e. ( E ` i ) } = { i e. dom E | -. N e/ ( E ` i ) }
25 7 24 eqtri 
 |-  J = { i e. dom E | -. N e/ ( E ` i ) }
26 20 21 25 3eqtr4i 
 |-  ( dom E \ I ) = J
27 26 a1i 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( dom E \ I ) = J )
28 27 fveq2d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` ( dom E \ I ) ) = ( # ` J ) )
29 19 28 oveq12d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( # ` ( E |` I ) ) + ( # ` ( dom E \ I ) ) ) = ( ( # ` P ) + ( # ` J ) ) )
30 16 29 eqtrd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` E ) = ( ( # ` P ) + ( # ` J ) ) )