Step | Hyp | Ref
| Expression |
1 | | finsumvtxdg2sstep.p |
. . 3
β’ π = (πΈ βΎ πΌ) |
2 | | finresfin 9270 |
. . . 4
β’ (πΈ β Fin β (πΈ βΎ πΌ) β Fin) |
3 | 2 | ad2antll 728 |
. . 3
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (πΈ βΎ πΌ) β Fin) |
4 | 1, 3 | eqeltrid 2838 |
. 2
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β π β Fin) |
5 | | difsnid 4814 |
. . . . . . . . 9
β’ (π β π β ((π β {π}) βͺ {π}) = π) |
6 | 5 | ad2antlr 726 |
. . . . . . . 8
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((π β {π}) βͺ {π}) = π) |
7 | 6 | eqcomd 2739 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β π = ((π β {π}) βͺ {π})) |
8 | 7 | sumeq1d 15647 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β Ξ£π£ β π ((VtxDegβπΊ)βπ£) = Ξ£π£ β ((π β {π}) βͺ {π})((VtxDegβπΊ)βπ£)) |
9 | | diffi 9179 |
. . . . . . . . 9
β’ (π β Fin β (π β {π}) β Fin) |
10 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π β Fin β§ πΈ β Fin) β (π β {π}) β Fin) |
11 | 10 | adantl 483 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (π β {π}) β Fin) |
12 | | simpr 486 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ π β π) β π β π) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β π β π) |
14 | | neldifsn 4796 |
. . . . . . . . 9
β’ Β¬
π β (π β {π}) |
15 | 14 | nelir 3050 |
. . . . . . . 8
β’ π β (π β {π}) |
16 | 15 | a1i 11 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β π β (π β {π})) |
17 | | dmfi 9330 |
. . . . . . . . . . 11
β’ (πΈ β Fin β dom πΈ β Fin) |
18 | 17 | ad2antll 728 |
. . . . . . . . . 10
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β dom πΈ β Fin) |
19 | 5 | eleq2d 2820 |
. . . . . . . . . . . . 13
β’ (π β π β (π£ β ((π β {π}) βͺ {π}) β π£ β π)) |
20 | 19 | biimpd 228 |
. . . . . . . . . . . 12
β’ (π β π β (π£ β ((π β {π}) βͺ {π}) β π£ β π)) |
21 | 20 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (π£ β ((π β {π}) βͺ {π}) β π£ β π)) |
22 | 21 | imp 408 |
. . . . . . . . . 10
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ π£ β ((π β {π}) βͺ {π})) β π£ β π) |
23 | | finsumvtxdg2sstep.v |
. . . . . . . . . . 11
β’ π = (VtxβπΊ) |
24 | | finsumvtxdg2sstep.e |
. . . . . . . . . . 11
β’ πΈ = (iEdgβπΊ) |
25 | | eqid 2733 |
. . . . . . . . . . 11
β’ dom πΈ = dom πΈ |
26 | 23, 24, 25 | vtxdgfisnn0 28732 |
. . . . . . . . . 10
β’ ((dom
πΈ β Fin β§ π£ β π) β ((VtxDegβπΊ)βπ£) β
β0) |
27 | 18, 22, 26 | syl2an2r 684 |
. . . . . . . . 9
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ π£ β ((π β {π}) βͺ {π})) β ((VtxDegβπΊ)βπ£) β
β0) |
28 | 27 | nn0zd 12584 |
. . . . . . . 8
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ π£ β ((π β {π}) βͺ {π})) β ((VtxDegβπΊ)βπ£) β β€) |
29 | 28 | ralrimiva 3147 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β βπ£ β ((π β {π}) βͺ {π})((VtxDegβπΊ)βπ£) β β€) |
30 | | fsumsplitsnun 15701 |
. . . . . . 7
β’ (((π β {π}) β Fin β§ (π β π β§ π β (π β {π})) β§ βπ£ β ((π β {π}) βͺ {π})((VtxDegβπΊ)βπ£) β β€) β Ξ£π£ β ((π β {π}) βͺ {π})((VtxDegβπΊ)βπ£) = (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + β¦π / π£β¦((VtxDegβπΊ)βπ£))) |
31 | 11, 13, 16, 29, 30 | syl121anc 1376 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β Ξ£π£ β ((π β {π}) βͺ {π})((VtxDegβπΊ)βπ£) = (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + β¦π / π£β¦((VtxDegβπΊ)βπ£))) |
32 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π£ = π β ((VtxDegβπΊ)βπ£) = ((VtxDegβπΊ)βπ)) |
33 | 32 | adantl 483 |
. . . . . . . . 9
β’ (((πΊ β UPGraph β§ π β π) β§ π£ = π) β ((VtxDegβπΊ)βπ£) = ((VtxDegβπΊ)βπ)) |
34 | 12, 33 | csbied 3932 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ π β π) β β¦π / π£β¦((VtxDegβπΊ)βπ£) = ((VtxDegβπΊ)βπ)) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β β¦π / π£β¦((VtxDegβπΊ)βπ£) = ((VtxDegβπΊ)βπ)) |
36 | 35 | oveq2d 7425 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + β¦π / π£β¦((VtxDegβπΊ)βπ£)) = (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((VtxDegβπΊ)βπ))) |
37 | 8, 31, 36 | 3eqtrd 2777 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β Ξ£π£ β π ((VtxDegβπΊ)βπ£) = (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((VtxDegβπΊ)βπ))) |
38 | 37 | adantr 482 |
. . . 4
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β Ξ£π£ β π ((VtxDegβπΊ)βπ£) = (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((VtxDegβπΊ)βπ))) |
39 | | finsumvtxdg2sstep.k |
. . . . . . . 8
β’ πΎ = (π β {π}) |
40 | | finsumvtxdg2sstep.i |
. . . . . . . 8
β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} |
41 | | finsumvtxdg2sstep.s |
. . . . . . . 8
β’ π = β¨πΎ, πβ© |
42 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = π β (πΈβπ) = (πΈβπ)) |
43 | 42 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = π β (π β (πΈβπ) β π β (πΈβπ))) |
44 | 43 | cbvrabv 3443 |
. . . . . . . 8
β’ {π β dom πΈ β£ π β (πΈβπ)} = {π β dom πΈ β£ π β (πΈβπ)} |
45 | 23, 24, 39, 40, 1, 41, 44 | finsumvtxdg2ssteplem2 28803 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((VtxDegβπΊ)βπ) = ((β―β{π β dom πΈ β£ π β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) |
46 | 45 | oveq2d 7425 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((VtxDegβπΊ)βπ)) = (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((β―β{π β dom πΈ β£ π β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})))) |
47 | 46 | adantr 482 |
. . . . 5
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((VtxDegβπΊ)βπ)) = (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((β―β{π β dom πΈ β£ π β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})))) |
48 | 23, 24, 39, 40, 1, 41, 44 | finsumvtxdg2ssteplem4 28805 |
. . . . 5
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((β―β{π β dom πΈ β£ π β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (2 Β· ((β―βπ) + (β―β{π β dom πΈ β£ π β (πΈβπ)})))) |
49 | 44 | fveq2i 6895 |
. . . . . . . 8
β’
(β―β{π
β dom πΈ β£ π β (πΈβπ)}) = (β―β{π β dom πΈ β£ π β (πΈβπ)}) |
50 | 49 | oveq2i 7420 |
. . . . . . 7
β’
((β―βπ) +
(β―β{π β
dom πΈ β£ π β (πΈβπ)})) = ((β―βπ) + (β―β{π β dom πΈ β£ π β (πΈβπ)})) |
51 | 50 | oveq2i 7420 |
. . . . . 6
β’ (2
Β· ((β―βπ)
+ (β―β{π β
dom πΈ β£ π β (πΈβπ)}))) = (2 Β· ((β―βπ) + (β―β{π β dom πΈ β£ π β (πΈβπ)}))) |
52 | 51 | a1i 11 |
. . . . 5
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (2 Β·
((β―βπ) +
(β―β{π β
dom πΈ β£ π β (πΈβπ)}))) = (2 Β· ((β―βπ) + (β―β{π β dom πΈ β£ π β (πΈβπ)})))) |
53 | 47, 48, 52 | 3eqtrd 2777 |
. . . 4
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((VtxDegβπΊ)βπ)) = (2 Β· ((β―βπ) + (β―β{π β dom πΈ β£ π β (πΈβπ)})))) |
54 | | eqid 2733 |
. . . . . . . 8
β’ {π β dom πΈ β£ π β (πΈβπ)} = {π β dom πΈ β£ π β (πΈβπ)} |
55 | 23, 24, 39, 40, 1, 41, 54 | finsumvtxdg2ssteplem1 28802 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (β―βπΈ) = ((β―βπ) + (β―β{π β dom πΈ β£ π β (πΈβπ)}))) |
56 | 55 | oveq2d 7425 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (2 Β·
(β―βπΈ)) = (2
Β· ((β―βπ)
+ (β―β{π β
dom πΈ β£ π β (πΈβπ)})))) |
57 | 56 | eqcomd 2739 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (2 Β·
((β―βπ) +
(β―β{π β
dom πΈ β£ π β (πΈβπ)}))) = (2 Β· (β―βπΈ))) |
58 | 57 | adantr 482 |
. . . 4
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (2 Β·
((β―βπ) +
(β―β{π β
dom πΈ β£ π β (πΈβπ)}))) = (2 Β· (β―βπΈ))) |
59 | 38, 53, 58 | 3eqtrd 2777 |
. . 3
β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β Ξ£π£ β π ((VtxDegβπΊ)βπ£) = (2 Β· (β―βπΈ))) |
60 | 59 | ex 414 |
. 2
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ)) β Ξ£π£ β π ((VtxDegβπΊ)βπ£) = (2 Β· (β―βπΈ)))) |
61 | 4, 60 | embantd 59 |
1
β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((π β Fin β Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β Ξ£π£ β π ((VtxDegβπΊ)βπ£) = (2 Β· (β―βπΈ)))) |