Step |
Hyp |
Ref |
Expression |
1 |
|
finsumvtxdgeven.v |
|- V = ( Vtx ` G ) |
2 |
|
finsumvtxdgeven.i |
|- I = ( iEdg ` G ) |
3 |
|
finsumvtxdgeven.d |
|- D = ( VtxDeg ` G ) |
4 |
1 2 3
|
finsumvtxdgeven |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || sum_ w e. V ( D ` w ) ) |
5 |
|
incom |
|- ( { v e. V | -. 2 || ( D ` v ) } i^i { v e. V | 2 || ( D ` v ) } ) = ( { v e. V | 2 || ( D ` v ) } i^i { v e. V | -. 2 || ( D ` v ) } ) |
6 |
|
rabnc |
|- ( { v e. V | 2 || ( D ` v ) } i^i { v e. V | -. 2 || ( D ` v ) } ) = (/) |
7 |
5 6
|
eqtri |
|- ( { v e. V | -. 2 || ( D ` v ) } i^i { v e. V | 2 || ( D ` v ) } ) = (/) |
8 |
7
|
a1i |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( { v e. V | -. 2 || ( D ` v ) } i^i { v e. V | 2 || ( D ` v ) } ) = (/) ) |
9 |
|
rabxm |
|- V = ( { v e. V | 2 || ( D ` v ) } u. { v e. V | -. 2 || ( D ` v ) } ) |
10 |
9
|
equncomi |
|- V = ( { v e. V | -. 2 || ( D ` v ) } u. { v e. V | 2 || ( D ` v ) } ) |
11 |
10
|
a1i |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> V = ( { v e. V | -. 2 || ( D ` v ) } u. { v e. V | 2 || ( D ` v ) } ) ) |
12 |
|
simp2 |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> V e. Fin ) |
13 |
3
|
fveq1i |
|- ( D ` w ) = ( ( VtxDeg ` G ) ` w ) |
14 |
|
dmfi |
|- ( I e. Fin -> dom I e. Fin ) |
15 |
14
|
3ad2ant3 |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> dom I e. Fin ) |
16 |
|
eqid |
|- dom I = dom I |
17 |
1 2 16
|
vtxdgfisnn0 |
|- ( ( dom I e. Fin /\ w e. V ) -> ( ( VtxDeg ` G ) ` w ) e. NN0 ) |
18 |
15 17
|
sylan |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. V ) -> ( ( VtxDeg ` G ) ` w ) e. NN0 ) |
19 |
18
|
nn0cnd |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. V ) -> ( ( VtxDeg ` G ) ` w ) e. CC ) |
20 |
13 19
|
eqeltrid |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. V ) -> ( D ` w ) e. CC ) |
21 |
8 11 12 20
|
fsumsplit |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> sum_ w e. V ( D ` w ) = ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) |
22 |
21
|
breq2d |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 || sum_ w e. V ( D ` w ) <-> 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) ) |
23 |
|
rabfi |
|- ( V e. Fin -> { v e. V | -. 2 || ( D ` v ) } e. Fin ) |
24 |
23
|
3ad2ant2 |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> { v e. V | -. 2 || ( D ` v ) } e. Fin ) |
25 |
|
elrabi |
|- ( w e. { v e. V | -. 2 || ( D ` v ) } -> w e. V ) |
26 |
15 25 17
|
syl2an |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | -. 2 || ( D ` v ) } ) -> ( ( VtxDeg ` G ) ` w ) e. NN0 ) |
27 |
26
|
nn0zd |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | -. 2 || ( D ` v ) } ) -> ( ( VtxDeg ` G ) ` w ) e. ZZ ) |
28 |
13 27
|
eqeltrid |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | -. 2 || ( D ` v ) } ) -> ( D ` w ) e. ZZ ) |
29 |
24 28
|
fsumzcl |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) e. ZZ ) |
30 |
29
|
adantr |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) e. ZZ ) |
31 |
|
fveq2 |
|- ( v = w -> ( D ` v ) = ( D ` w ) ) |
32 |
31
|
breq2d |
|- ( v = w -> ( 2 || ( D ` v ) <-> 2 || ( D ` w ) ) ) |
33 |
32
|
notbid |
|- ( v = w -> ( -. 2 || ( D ` v ) <-> -. 2 || ( D ` w ) ) ) |
34 |
33
|
elrab |
|- ( w e. { v e. V | -. 2 || ( D ` v ) } <-> ( w e. V /\ -. 2 || ( D ` w ) ) ) |
35 |
34
|
simprbi |
|- ( w e. { v e. V | -. 2 || ( D ` v ) } -> -. 2 || ( D ` w ) ) |
36 |
35
|
adantl |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | -. 2 || ( D ` v ) } ) -> -. 2 || ( D ` w ) ) |
37 |
24 28 36
|
sumodd |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) <-> 2 || sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) ) ) |
38 |
37
|
notbid |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) <-> -. 2 || sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) ) ) |
39 |
38
|
biimpa |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> -. 2 || sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) ) |
40 |
|
rabfi |
|- ( V e. Fin -> { v e. V | 2 || ( D ` v ) } e. Fin ) |
41 |
40
|
3ad2ant2 |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> { v e. V | 2 || ( D ` v ) } e. Fin ) |
42 |
|
elrabi |
|- ( w e. { v e. V | 2 || ( D ` v ) } -> w e. V ) |
43 |
15 42 17
|
syl2an |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | 2 || ( D ` v ) } ) -> ( ( VtxDeg ` G ) ` w ) e. NN0 ) |
44 |
43
|
nn0zd |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | 2 || ( D ` v ) } ) -> ( ( VtxDeg ` G ) ` w ) e. ZZ ) |
45 |
13 44
|
eqeltrid |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | 2 || ( D ` v ) } ) -> ( D ` w ) e. ZZ ) |
46 |
41 45
|
fsumzcl |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) e. ZZ ) |
47 |
46
|
adantr |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) e. ZZ ) |
48 |
32
|
elrab |
|- ( w e. { v e. V | 2 || ( D ` v ) } <-> ( w e. V /\ 2 || ( D ` w ) ) ) |
49 |
48
|
simprbi |
|- ( w e. { v e. V | 2 || ( D ` v ) } -> 2 || ( D ` w ) ) |
50 |
49
|
adantl |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | 2 || ( D ` v ) } ) -> 2 || ( D ` w ) ) |
51 |
41 45 50
|
sumeven |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) |
52 |
51
|
adantr |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> 2 || sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) |
53 |
|
opeo |
|- ( ( ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) e. ZZ /\ -. 2 || sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) ) /\ ( sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) e. ZZ /\ 2 || sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) -> -. 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) |
54 |
30 39 47 52 53
|
syl22anc |
|- ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> -. 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) |
55 |
54
|
ex |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) -> -. 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) ) |
56 |
55
|
con4d |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) ) |
57 |
22 56
|
sylbid |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 || sum_ w e. V ( D ` w ) -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) ) |
58 |
4 57
|
mpd |
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) |