Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem4

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 finsumvtxdg2ssteplem4 
|- ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) ) -> ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( 2 x. ( ( # ` 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 1 2 3 4 5 6 7 vtxdginducedm1fi 
 |-  ( E e. Fin -> A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) + ( # ` { i e. J | v e. ( E ` i ) } ) ) )
9 8 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) + ( # ` { i e. J | v e. ( E ` i ) } ) ) )
10 9 sumeq2d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = sum_ v e. ( V \ { N } ) ( ( ( VtxDeg ` S ) ` v ) + ( # ` { i e. J | v e. ( E ` i ) } ) ) )
11 diffi 
 |-  ( V e. Fin -> ( V \ { N } ) e. Fin )
12 11 adantr 
 |-  ( ( V e. Fin /\ E e. Fin ) -> ( V \ { N } ) e. Fin )
13 12 adantl 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( V \ { N } ) e. Fin )
14 5 dmeqi 
 |-  dom P = dom ( E |` I )
15 finresfin 
 |-  ( E e. Fin -> ( E |` I ) e. Fin )
16 dmfi 
 |-  ( ( E |` I ) e. Fin -> dom ( E |` I ) e. Fin )
17 15 16 syl 
 |-  ( E e. Fin -> dom ( E |` I ) e. Fin )
18 14 17 eqeltrid 
 |-  ( E e. Fin -> dom P e. Fin )
19 18 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> dom P e. Fin )
20 3 eqcomi 
 |-  ( V \ { N } ) = K
21 20 eleq2i 
 |-  ( v e. ( V \ { N } ) <-> v e. K )
22 21 biimpi 
 |-  ( v e. ( V \ { N } ) -> v e. K )
23 6 fveq2i 
 |-  ( Vtx ` S ) = ( Vtx ` <. K , P >. )
24 1 fvexi 
 |-  V e. _V
25 24 difexi 
 |-  ( V \ { N } ) e. _V
26 3 25 eqeltri 
 |-  K e. _V
27 2 fvexi 
 |-  E e. _V
28 27 resex 
 |-  ( E |` I ) e. _V
29 5 28 eqeltri 
 |-  P e. _V
30 26 29 opvtxfvi 
 |-  ( Vtx ` <. K , P >. ) = K
31 23 30 eqtr2i 
 |-  K = ( Vtx ` S )
32 1 2 3 4 5 6 vtxdginducedm1lem1 
 |-  ( iEdg ` S ) = P
33 32 eqcomi 
 |-  P = ( iEdg ` S )
34 eqid 
 |-  dom P = dom P
35 31 33 34 vtxdgfisnn0 
 |-  ( ( dom P e. Fin /\ v e. K ) -> ( ( VtxDeg ` S ) ` v ) e. NN0 )
36 35 nn0cnd 
 |-  ( ( dom P e. Fin /\ v e. K ) -> ( ( VtxDeg ` S ) ` v ) e. CC )
37 19 22 36 syl2an 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ v e. ( V \ { N } ) ) -> ( ( VtxDeg ` S ) ` v ) e. CC )
38 dmfi 
 |-  ( E e. Fin -> dom E e. Fin )
39 rabfi 
 |-  ( dom E e. Fin -> { i e. dom E | N e. ( E ` i ) } e. Fin )
40 38 39 syl 
 |-  ( E e. Fin -> { i e. dom E | N e. ( E ` i ) } e. Fin )
41 7 40 eqeltrid 
 |-  ( E e. Fin -> J e. Fin )
42 rabfi 
 |-  ( J e. Fin -> { i e. J | v e. ( E ` i ) } e. Fin )
43 hashcl 
 |-  ( { i e. J | v e. ( E ` i ) } e. Fin -> ( # ` { i e. J | v e. ( E ` i ) } ) e. NN0 )
44 41 42 43 3syl 
 |-  ( E e. Fin -> ( # ` { i e. J | v e. ( E ` i ) } ) e. NN0 )
45 44 nn0cnd 
 |-  ( E e. Fin -> ( # ` { i e. J | v e. ( E ` i ) } ) e. CC )
46 45 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` { i e. J | v e. ( E ` i ) } ) e. CC )
47 46 adantr 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ v e. ( V \ { N } ) ) -> ( # ` { i e. J | v e. ( E ` i ) } ) e. CC )
48 13 37 47 fsumadd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> sum_ v e. ( V \ { N } ) ( ( ( VtxDeg ` S ) ` v ) + ( # ` { i e. J | v e. ( E ` i ) } ) ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` S ) ` v ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) )
49 10 48 eqtrd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` S ) ` v ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) )
50 3 sumeq1i 
 |-  sum_ v e. K ( ( VtxDeg ` S ) ` v ) = sum_ v e. ( V \ { N } ) ( ( VtxDeg ` S ) ` v )
51 50 eqeq1i 
 |-  ( sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) <-> sum_ v e. ( V \ { N } ) ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) )
52 oveq1 
 |-  ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) -> ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` S ) ` v ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) = ( ( 2 x. ( # ` P ) ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) )
53 51 52 sylbi 
 |-  ( sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) -> ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` S ) ` v ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) = ( ( 2 x. ( # ` P ) ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) )
54 49 53 sylan9eq 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) ) -> sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( 2 x. ( # ` P ) ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) )
55 54 oveq1d 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) ) -> ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( ( ( 2 x. ( # ` P ) ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) )
56 45 adantl 
 |-  ( ( V e. Fin /\ E e. Fin ) -> ( # ` { i e. J | v e. ( E ` i ) } ) e. CC )
57 56 adantr 
 |-  ( ( ( V e. Fin /\ E e. Fin ) /\ v e. ( V \ { N } ) ) -> ( # ` { i e. J | v e. ( E ` i ) } ) e. CC )
58 12 57 fsumcl 
 |-  ( ( V e. Fin /\ E e. Fin ) -> sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) e. CC )
59 hashcl 
 |-  ( J e. Fin -> ( # ` J ) e. NN0 )
60 41 59 syl 
 |-  ( E e. Fin -> ( # ` J ) e. NN0 )
61 60 nn0cnd 
 |-  ( E e. Fin -> ( # ` J ) e. CC )
62 61 adantl 
 |-  ( ( V e. Fin /\ E e. Fin ) -> ( # ` J ) e. CC )
63 rabfi 
 |-  ( dom E e. Fin -> { i e. dom E | ( E ` i ) = { N } } e. Fin )
64 hashcl 
 |-  ( { i e. dom E | ( E ` i ) = { N } } e. Fin -> ( # ` { i e. dom E | ( E ` i ) = { N } } ) e. NN0 )
65 38 63 64 3syl 
 |-  ( E e. Fin -> ( # ` { i e. dom E | ( E ` i ) = { N } } ) e. NN0 )
66 65 nn0cnd 
 |-  ( E e. Fin -> ( # ` { i e. dom E | ( E ` i ) = { N } } ) e. CC )
67 66 adantl 
 |-  ( ( V e. Fin /\ E e. Fin ) -> ( # ` { i e. dom E | ( E ` i ) = { N } } ) e. CC )
68 58 62 67 add12d 
 |-  ( ( V e. Fin /\ E e. Fin ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( ( # ` J ) + ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) )
69 68 adantl 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( ( # ` J ) + ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) )
70 1 2 3 4 5 6 7 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 ) )
71 70 oveq2d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( # ` J ) + ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( ( # ` J ) + ( # ` J ) ) )
72 61 2timesd 
 |-  ( E e. Fin -> ( 2 x. ( # ` J ) ) = ( ( # ` J ) + ( # ` J ) ) )
73 72 eqcomd 
 |-  ( E e. Fin -> ( ( # ` J ) + ( # ` J ) ) = ( 2 x. ( # ` J ) ) )
74 73 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( # ` J ) + ( # ` J ) ) = ( 2 x. ( # ` J ) ) )
75 69 71 74 3eqtrd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( 2 x. ( # ` J ) ) )
76 75 oveq2d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( 2 x. ( # ` P ) ) + ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) ) = ( ( 2 x. ( # ` P ) ) + ( 2 x. ( # ` J ) ) ) )
77 2cnd 
 |-  ( E e. Fin -> 2 e. CC )
78 5 15 eqeltrid 
 |-  ( E e. Fin -> P e. Fin )
79 hashcl 
 |-  ( P e. Fin -> ( # ` P ) e. NN0 )
80 78 79 syl 
 |-  ( E e. Fin -> ( # ` P ) e. NN0 )
81 80 nn0cnd 
 |-  ( E e. Fin -> ( # ` P ) e. CC )
82 77 81 mulcld 
 |-  ( E e. Fin -> ( 2 x. ( # ` P ) ) e. CC )
83 82 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( 2 x. ( # ` P ) ) e. CC )
84 58 adantl 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) e. CC )
85 61 66 addcld 
 |-  ( E e. Fin -> ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) e. CC )
86 85 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) e. CC )
87 83 84 86 addassd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( ( 2 x. ( # ` P ) ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( ( 2 x. ( # ` P ) ) + ( sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) ) )
88 2cnd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> 2 e. CC )
89 81 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` P ) e. CC )
90 61 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` J ) e. CC )
91 88 89 90 adddid 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( 2 x. ( ( # ` P ) + ( # ` J ) ) ) = ( ( 2 x. ( # ` P ) ) + ( 2 x. ( # ` J ) ) ) )
92 76 87 91 3eqtr4d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( ( 2 x. ( # ` P ) ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( 2 x. ( ( # ` P ) + ( # ` J ) ) ) )
93 92 adantr 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) ) -> ( ( ( 2 x. ( # ` P ) ) + sum_ v e. ( V \ { N } ) ( # ` { i e. J | v e. ( E ` i ) } ) ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( 2 x. ( ( # ` P ) + ( # ` J ) ) ) )
94 55 93 eqtrd 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) ) -> ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( # ` J ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( 2 x. ( ( # ` P ) + ( # ` J ) ) ) )