Step | Hyp | Ref
| Expression |
1 | | finsumvtxdg2sstep.v |
. . . . . . . 8
β’ π = (VtxβπΊ) |
2 | | finsumvtxdg2sstep.e |
. . . . . . . 8
β’ πΈ = (iEdgβπΊ) |
3 | | finsumvtxdg2sstep.k |
. . . . . . . 8
β’ πΎ = (π β {π}) |
4 | | finsumvtxdg2sstep.i |
. . . . . . . 8
β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} |
5 | | finsumvtxdg2sstep.p |
. . . . . . . 8
β’ π = (πΈ βΎ πΌ) |
6 | | finsumvtxdg2sstep.s |
. . . . . . . 8
β’ π = β¨πΎ, πβ© |
7 | | finsumvtxdg2ssteplem.j |
. . . . . . . 8
β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} |
8 | 1, 2, 3, 4, 5, 6, 7 | vtxdginducedm1fi 28534 |
. . . . . . 7
β’ (πΈ β Fin β βπ£ β (π β {π})((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)}))) |
9 | 8 | ad2antll 728 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β βπ£ β (π β {π})((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)}))) |
10 | 9 | sumeq2d 15594 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) = Ξ£π£ β (π β {π})(((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)}))) |
11 | | diffi 9130 |
. . . . . . . 8
β’ (π β Fin β (π β {π}) β Fin) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β Fin β§ πΈ β Fin) β (π β {π}) β Fin) |
13 | 12 | adantl 483 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (π β {π}) β Fin) |
14 | 5 | dmeqi 5865 |
. . . . . . . . 9
β’ dom π = dom (πΈ βΎ πΌ) |
15 | | finresfin 9221 |
. . . . . . . . . 10
β’ (πΈ β Fin β (πΈ βΎ πΌ) β Fin) |
16 | | dmfi 9281 |
. . . . . . . . . 10
β’ ((πΈ βΎ πΌ) β Fin β dom (πΈ βΎ πΌ) β Fin) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
β’ (πΈ β Fin β dom (πΈ βΎ πΌ) β Fin) |
18 | 14, 17 | eqeltrid 2842 |
. . . . . . . 8
β’ (πΈ β Fin β dom π β Fin) |
19 | 18 | ad2antll 728 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β dom π β Fin) |
20 | 3 | eqcomi 2746 |
. . . . . . . . 9
β’ (π β {π}) = πΎ |
21 | 20 | eleq2i 2830 |
. . . . . . . 8
β’ (π£ β (π β {π}) β π£ β πΎ) |
22 | 21 | biimpi 215 |
. . . . . . 7
β’ (π£ β (π β {π}) β π£ β πΎ) |
23 | 6 | fveq2i 6850 |
. . . . . . . . . 10
β’
(Vtxβπ) =
(Vtxββ¨πΎ, πβ©) |
24 | 1 | fvexi 6861 |
. . . . . . . . . . . . 13
β’ π β V |
25 | 24 | difexi 5290 |
. . . . . . . . . . . 12
β’ (π β {π}) β V |
26 | 3, 25 | eqeltri 2834 |
. . . . . . . . . . 11
β’ πΎ β V |
27 | 2 | fvexi 6861 |
. . . . . . . . . . . . 13
β’ πΈ β V |
28 | 27 | resex 5990 |
. . . . . . . . . . . 12
β’ (πΈ βΎ πΌ) β V |
29 | 5, 28 | eqeltri 2834 |
. . . . . . . . . . 11
β’ π β V |
30 | 26, 29 | opvtxfvi 28002 |
. . . . . . . . . 10
β’
(Vtxββ¨πΎ,
πβ©) = πΎ |
31 | 23, 30 | eqtr2i 2766 |
. . . . . . . . 9
β’ πΎ = (Vtxβπ) |
32 | 1, 2, 3, 4, 5, 6 | vtxdginducedm1lem1 28529 |
. . . . . . . . . 10
β’
(iEdgβπ) =
π |
33 | 32 | eqcomi 2746 |
. . . . . . . . 9
β’ π = (iEdgβπ) |
34 | | eqid 2737 |
. . . . . . . . 9
β’ dom π = dom π |
35 | 31, 33, 34 | vtxdgfisnn0 28465 |
. . . . . . . 8
β’ ((dom
π β Fin β§ π£ β πΎ) β ((VtxDegβπ)βπ£) β
β0) |
36 | 35 | nn0cnd 12482 |
. . . . . . 7
β’ ((dom
π β Fin β§ π£ β πΎ) β ((VtxDegβπ)βπ£) β β) |
37 | 19, 22, 36 | syl2an 597 |
. . . . . 6
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ π£ β (π β {π})) β ((VtxDegβπ)βπ£) β β) |
38 | | dmfi 9281 |
. . . . . . . . . . . 12
β’ (πΈ β Fin β dom πΈ β Fin) |
39 | | rabfi 9220 |
. . . . . . . . . . . 12
β’ (dom
πΈ β Fin β {π β dom πΈ β£ π β (πΈβπ)} β Fin) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
β’ (πΈ β Fin β {π β dom πΈ β£ π β (πΈβπ)} β Fin) |
41 | 7, 40 | eqeltrid 2842 |
. . . . . . . . . 10
β’ (πΈ β Fin β π½ β Fin) |
42 | | rabfi 9220 |
. . . . . . . . . 10
β’ (π½ β Fin β {π β π½ β£ π£ β (πΈβπ)} β Fin) |
43 | | hashcl 14263 |
. . . . . . . . . 10
β’ ({π β π½ β£ π£ β (πΈβπ)} β Fin β (β―β{π β π½ β£ π£ β (πΈβπ)}) β
β0) |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . . . 9
β’ (πΈ β Fin β
(β―β{π β
π½ β£ π£ β (πΈβπ)}) β
β0) |
45 | 44 | nn0cnd 12482 |
. . . . . . . 8
β’ (πΈ β Fin β
(β―β{π β
π½ β£ π£ β (πΈβπ)}) β β) |
46 | 45 | ad2antll 728 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (β―β{π β π½ β£ π£ β (πΈβπ)}) β β) |
47 | 46 | adantr 482 |
. . . . . 6
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ π£ β (π β {π})) β (β―β{π β π½ β£ π£ β (πΈβπ)}) β β) |
48 | 13, 37, 47 | fsumadd 15632 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β Ξ£π£ β (π β {π})(((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)})) = (Ξ£π£ β (π β {π})((VtxDegβπ)βπ£) + Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}))) |
49 | 10, 48 | eqtrd 2777 |
. . . 4
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) = (Ξ£π£ β (π β {π})((VtxDegβπ)βπ£) + Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}))) |
50 | 3 | sumeq1i 15590 |
. . . . . 6
β’
Ξ£π£ β
πΎ ((VtxDegβπ)βπ£) = Ξ£π£ β (π β {π})((VtxDegβπ)βπ£) |
51 | 50 | eqeq1i 2742 |
. . . . 5
β’
(Ξ£π£ β
πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ)) β Ξ£π£ β (π β {π})((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) |
52 | | oveq1 7369 |
. . . . 5
β’
(Ξ£π£ β
(π β {π})((VtxDegβπ)βπ£) = (2 Β· (β―βπ)) β (Ξ£π£ β (π β {π})((VtxDegβπ)βπ£) + Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)})) = ((2 Β· (β―βπ)) + Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}))) |
53 | 51, 52 | sylbi 216 |
. . . 4
β’
(Ξ£π£ β
πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ)) β (Ξ£π£ β (π β {π})((VtxDegβπ)βπ£) + Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)})) = ((2 Β· (β―βπ)) + Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}))) |
54 | 49, 53 | sylan9eq 2797 |
. . 3
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) = ((2 Β· (β―βπ)) + Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}))) |
55 | 54 | oveq1d 7377 |
. 2
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (((2 Β· (β―βπ)) + Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)})) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})))) |
56 | 45 | adantl 483 |
. . . . . . . . . 10
β’ ((π β Fin β§ πΈ β Fin) β
(β―β{π β
π½ β£ π£ β (πΈβπ)}) β β) |
57 | 56 | adantr 482 |
. . . . . . . . 9
β’ (((π β Fin β§ πΈ β Fin) β§ π£ β (π β {π})) β (β―β{π β π½ β£ π£ β (πΈβπ)}) β β) |
58 | 12, 57 | fsumcl 15625 |
. . . . . . . 8
β’ ((π β Fin β§ πΈ β Fin) β Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) β β) |
59 | | hashcl 14263 |
. . . . . . . . . . 11
β’ (π½ β Fin β
(β―βπ½) β
β0) |
60 | 41, 59 | syl 17 |
. . . . . . . . . 10
β’ (πΈ β Fin β
(β―βπ½) β
β0) |
61 | 60 | nn0cnd 12482 |
. . . . . . . . 9
β’ (πΈ β Fin β
(β―βπ½) β
β) |
62 | 61 | adantl 483 |
. . . . . . . 8
β’ ((π β Fin β§ πΈ β Fin) β
(β―βπ½) β
β) |
63 | | rabfi 9220 |
. . . . . . . . . . 11
β’ (dom
πΈ β Fin β {π β dom πΈ β£ (πΈβπ) = {π}} β Fin) |
64 | | hashcl 14263 |
. . . . . . . . . . 11
β’ ({π β dom πΈ β£ (πΈβπ) = {π}} β Fin β (β―β{π β dom πΈ β£ (πΈβπ) = {π}}) β
β0) |
65 | 38, 63, 64 | 3syl 18 |
. . . . . . . . . 10
β’ (πΈ β Fin β
(β―β{π β
dom πΈ β£ (πΈβπ) = {π}}) β
β0) |
66 | 65 | nn0cnd 12482 |
. . . . . . . . 9
β’ (πΈ β Fin β
(β―β{π β
dom πΈ β£ (πΈβπ) = {π}}) β β) |
67 | 66 | adantl 483 |
. . . . . . . 8
β’ ((π β Fin β§ πΈ β Fin) β
(β―β{π β
dom πΈ β£ (πΈβπ) = {π}}) β β) |
68 | 58, 62, 67 | add12d 11388 |
. . . . . . 7
β’ ((π β Fin β§ πΈ β Fin) β
(Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = ((β―βπ½) + (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})))) |
69 | 68 | adantl 483 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = ((β―βπ½) + (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})))) |
70 | 1, 2, 3, 4, 5, 6, 7 | finsumvtxdg2ssteplem3 28537 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})) = (β―βπ½)) |
71 | 70 | oveq2d 7378 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((β―βπ½) + (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = ((β―βπ½) + (β―βπ½))) |
72 | 61 | 2timesd 12403 |
. . . . . . . 8
β’ (πΈ β Fin β (2 Β·
(β―βπ½)) =
((β―βπ½) +
(β―βπ½))) |
73 | 72 | eqcomd 2743 |
. . . . . . 7
β’ (πΈ β Fin β
((β―βπ½) +
(β―βπ½)) = (2
Β· (β―βπ½))) |
74 | 73 | ad2antll 728 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((β―βπ½) + (β―βπ½)) = (2 Β·
(β―βπ½))) |
75 | 69, 71, 74 | 3eqtrd 2781 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (2 Β· (β―βπ½))) |
76 | 75 | oveq2d 7378 |
. . . 4
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((2 Β·
(β―βπ)) +
(Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})))) = ((2 Β· (β―βπ)) + (2 Β·
(β―βπ½)))) |
77 | | 2cnd 12238 |
. . . . . . 7
β’ (πΈ β Fin β 2 β
β) |
78 | 5, 15 | eqeltrid 2842 |
. . . . . . . . 9
β’ (πΈ β Fin β π β Fin) |
79 | | hashcl 14263 |
. . . . . . . . 9
β’ (π β Fin β
(β―βπ) β
β0) |
80 | 78, 79 | syl 17 |
. . . . . . . 8
β’ (πΈ β Fin β
(β―βπ) β
β0) |
81 | 80 | nn0cnd 12482 |
. . . . . . 7
β’ (πΈ β Fin β
(β―βπ) β
β) |
82 | 77, 81 | mulcld 11182 |
. . . . . 6
β’ (πΈ β Fin β (2 Β·
(β―βπ)) β
β) |
83 | 82 | ad2antll 728 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (2 Β·
(β―βπ)) β
β) |
84 | 58 | adantl 483 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) β β) |
85 | 61, 66 | addcld 11181 |
. . . . . 6
β’ (πΈ β Fin β
((β―βπ½) +
(β―β{π β
dom πΈ β£ (πΈβπ) = {π}})) β β) |
86 | 85 | ad2antll 728 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})) β β) |
87 | 83, 84, 86 | addassd 11184 |
. . . 4
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (((2 Β·
(β―βπ)) +
Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)})) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = ((2 Β· (β―βπ)) + (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))))) |
88 | | 2cnd 12238 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β 2 β
β) |
89 | 81 | ad2antll 728 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (β―βπ) β
β) |
90 | 61 | ad2antll 728 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (β―βπ½) β
β) |
91 | 88, 89, 90 | adddid 11186 |
. . . 4
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (2 Β·
((β―βπ) +
(β―βπ½))) = ((2
Β· (β―βπ))
+ (2 Β· (β―βπ½)))) |
92 | 76, 87, 91 | 3eqtr4d 2787 |
. . 3
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (((2 Β·
(β―βπ)) +
Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)})) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (2 Β· ((β―βπ) + (β―βπ½)))) |
93 | 92 | adantr 482 |
. 2
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (((2 Β·
(β―βπ)) +
Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)})) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (2 Β· ((β―βπ) + (β―βπ½)))) |
94 | 55, 93 | eqtrd 2777 |
1
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (2 Β· ((β―βπ) + (β―βπ½)))) |