Metamath Proof Explorer

Theorem finsumvtxdg2sstep

Description: Induction step of finsumvtxdg2size : In a finite pseudograph of finite size, the sum of the degrees of all vertices of the pseudograph is twice the size of the pseudograph if the sum of the degrees of all vertices of the subgraph of the pseudograph not containing one of the vertices is twice the size of the subgraph. (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 >.
Assertion finsumvtxdg2sstep 
|- ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( P e. Fin -> sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) ) -> sum_ v e. V ( ( VtxDeg ` G ) ` v ) = ( 2 x. ( # ` E ) ) ) )

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 finresfin 
 |-  ( E e. Fin -> ( E |` I ) e. Fin )
8 7 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( E |` I ) e. Fin )
9 5 8 eqeltrid 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> P e. Fin )
10 difsnid 
 |-  ( N e. V -> ( ( V \ { N } ) u. { N } ) = V )
11 10 ad2antlr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( V \ { N } ) u. { N } ) = V )
12 11 eqcomd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> V = ( ( V \ { N } ) u. { N } ) )
13 12 sumeq1d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> sum_ v e. V ( ( VtxDeg ` G ) ` v ) = sum_ v e. ( ( V \ { N } ) u. { N } ) ( ( VtxDeg ` G ) ` v ) )
14 diffi 
 |-  ( V e. Fin -> ( V \ { N } ) e. Fin )
15 14 adantr 
 |-  ( ( V e. Fin /\ E e. Fin ) -> ( V \ { N } ) e. Fin )
16 15 adantl 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( V \ { N } ) e. Fin )
17 simpr 
 |-  ( ( G e. UPGraph /\ N e. V ) -> N e. V )
18 17 adantr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> N e. V )
19 neldifsn 
 |-  -. N e. ( V \ { N } )
20 19 nelir 
 |-  N e/ ( V \ { N } )
21 20 a1i 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> N e/ ( V \ { N } ) )
22 dmfi 
 |-  ( E e. Fin -> dom E e. Fin )
23 22 ad2antll 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> dom E e. Fin )
24 10 eleq2d 
 |-  ( N e. V -> ( v e. ( ( V \ { N } ) u. { N } ) <-> v e. V ) )
25 24 biimpd 
 |-  ( N e. V -> ( v e. ( ( V \ { N } ) u. { N } ) -> v e. V ) )
26 25 ad2antlr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( v e. ( ( V \ { N } ) u. { N } ) -> v e. V ) )
27 26 imp 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ v e. ( ( V \ { N } ) u. { N } ) ) -> v e. V )
28 eqid 
 |-  dom E = dom E
29 1 2 28 vtxdgfisnn0 
 |-  ( ( dom E e. Fin /\ v e. V ) -> ( ( VtxDeg ` G ) ` v ) e. NN0 )
30 23 27 29 syl2an2r 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ v e. ( ( V \ { N } ) u. { N } ) ) -> ( ( VtxDeg ` G ) ` v ) e. NN0 )
31 30 nn0zd 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) /\ v e. ( ( V \ { N } ) u. { N } ) ) -> ( ( VtxDeg ` G ) ` v ) e. ZZ )
32 31 ralrimiva 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> A. v e. ( ( V \ { N } ) u. { N } ) ( ( VtxDeg ` G ) ` v ) e. ZZ )
33 fsumsplitsnun 
 |-  ( ( ( V \ { N } ) e. Fin /\ ( N e. V /\ N e/ ( V \ { N } ) ) /\ A. v e. ( ( V \ { N } ) u. { N } ) ( ( VtxDeg ` G ) ` v ) e. ZZ ) -> sum_ v e. ( ( V \ { N } ) u. { N } ) ( ( VtxDeg ` G ) ` v ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + [_ N / v ]_ ( ( VtxDeg ` G ) ` v ) ) )
34 16 18 21 32 33 syl121anc 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> sum_ v e. ( ( V \ { N } ) u. { N } ) ( ( VtxDeg ` G ) ` v ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + [_ N / v ]_ ( ( VtxDeg ` G ) ` v ) ) )
35 fveq2 
 |-  ( v = N -> ( ( VtxDeg ` G ) ` v ) = ( ( VtxDeg ` G ) ` N ) )
36 35 adantl 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ v = N ) -> ( ( VtxDeg ` G ) ` v ) = ( ( VtxDeg ` G ) ` N ) )
37 17 36 csbied 
 |-  ( ( G e. UPGraph /\ N e. V ) -> [_ N / v ]_ ( ( VtxDeg ` G ) ` v ) = ( ( VtxDeg ` G ) ` N ) )
38 37 adantr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> [_ N / v ]_ ( ( VtxDeg ` G ) ` v ) = ( ( VtxDeg ` G ) ` N ) )
39 38 oveq2d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + [_ N / v ]_ ( ( VtxDeg ` G ) ` v ) ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( VtxDeg ` G ) ` N ) ) )
40 13 34 39 3eqtrd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> sum_ v e. V ( ( VtxDeg ` G ) ` v ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( VtxDeg ` G ) ` N ) ) )
41 40 adantr 
 |-  ( ( ( ( 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 ( ( VtxDeg ` G ) ` v ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( VtxDeg ` G ) ` N ) ) )
42 fveq2 
 |-  ( j = i -> ( E ` j ) = ( E ` i ) )
43 42 eleq2d 
 |-  ( j = i -> ( N e. ( E ` j ) <-> N e. ( E ` i ) ) )
44 43 cbvrabv 
 |-  { j e. dom E | N e. ( E ` j ) } = { i e. dom E | N e. ( E ` i ) }
45 1 2 3 4 5 6 44 finsumvtxdg2ssteplem2 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { j e. dom E | N e. ( E ` j ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) )
46 45 oveq2d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( VtxDeg ` G ) ` N ) ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( # ` { j e. dom E | N e. ( E ` j ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) )
47 46 adantr 
 |-  ( ( ( ( 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 ) + ( ( VtxDeg ` G ) ` N ) ) = ( sum_ v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) + ( ( # ` { j e. dom E | N e. ( E ` j ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) )
48 1 2 3 4 5 6 44 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 e. dom E | N e. ( E ` j ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) ) = ( 2 x. ( ( # ` P ) + ( # ` { j e. dom E | N e. ( E ` j ) } ) ) ) )
49 44 fveq2i 
 |-  ( # ` { j e. dom E | N e. ( E ` j ) } ) = ( # ` { i e. dom E | N e. ( E ` i ) } )
50 49 oveq2i 
 |-  ( ( # ` P ) + ( # ` { j e. dom E | N e. ( E ` j ) } ) ) = ( ( # ` P ) + ( # ` { i e. dom E | N e. ( E ` i ) } ) )
51 50 oveq2i 
 |-  ( 2 x. ( ( # ` P ) + ( # ` { j e. dom E | N e. ( E ` j ) } ) ) ) = ( 2 x. ( ( # ` P ) + ( # ` { i e. dom E | N e. ( E ` i ) } ) ) )
52 51 a1i 
 |-  ( ( ( ( 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 ) + ( # ` { j e. dom E | N e. ( E ` j ) } ) ) ) = ( 2 x. ( ( # ` P ) + ( # ` { i e. dom E | N e. ( E ` i ) } ) ) ) )
53 47 48 52 3eqtrd 
 |-  ( ( ( ( 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 ) + ( ( VtxDeg ` G ) ` N ) ) = ( 2 x. ( ( # ` P ) + ( # ` { i e. dom E | N e. ( E ` i ) } ) ) ) )
54 eqid 
 |-  { i e. dom E | N e. ( E ` i ) } = { i e. dom E | N e. ( E ` i ) }
55 1 2 3 4 5 6 54 finsumvtxdg2ssteplem1 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( # ` E ) = ( ( # ` P ) + ( # ` { i e. dom E | N e. ( E ` i ) } ) ) )
56 55 oveq2d 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( 2 x. ( # ` E ) ) = ( 2 x. ( ( # ` P ) + ( # ` { i e. dom E | N e. ( E ` i ) } ) ) ) )
57 56 eqcomd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( 2 x. ( ( # ` P ) + ( # ` { i e. dom E | N e. ( E ` i ) } ) ) ) = ( 2 x. ( # ` E ) ) )
58 57 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 ) + ( # ` { i e. dom E | N e. ( E ` i ) } ) ) ) = ( 2 x. ( # ` E ) ) )
59 41 53 58 3eqtrd 
 |-  ( ( ( ( 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 ( ( VtxDeg ` G ) ` v ) = ( 2 x. ( # ` E ) ) )
60 59 ex 
 |-  ( ( ( 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 ( ( VtxDeg ` G ) ` v ) = ( 2 x. ( # ` E ) ) ) )
61 9 60 embantd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ ( V e. Fin /\ E e. Fin ) ) -> ( ( P e. Fin -> sum_ v e. K ( ( VtxDeg ` S ) ` v ) = ( 2 x. ( # ` P ) ) ) -> sum_ v e. V ( ( VtxDeg ` G ) ` v ) = ( 2 x. ( # ` E ) ) ) )