Step | Hyp | Ref
| Expression |
1 | | vtxdginducedm1.v |
. . 3
β’ π = (VtxβπΊ) |
2 | | vtxdginducedm1.e |
. . 3
β’ πΈ = (iEdgβπΊ) |
3 | | vtxdginducedm1.k |
. . 3
β’ πΎ = (π β {π}) |
4 | | vtxdginducedm1.i |
. . 3
β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} |
5 | | vtxdginducedm1.p |
. . 3
β’ π = (πΈ βΎ πΌ) |
6 | | vtxdginducedm1.s |
. . 3
β’ π = β¨πΎ, πβ© |
7 | | vtxdginducedm1.j |
. . 3
β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} |
8 | 1, 2, 3, 4, 5, 6, 7 | vtxdginducedm1 28540 |
. 2
β’
βπ£ β
(π β {π})((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) +π (β―β{π β π½ β£ π£ β (πΈβπ)})) |
9 | 5 | dmeqi 5864 |
. . . . . . . . 9
β’ dom π = dom (πΈ βΎ πΌ) |
10 | | finresfin 9220 |
. . . . . . . . . 10
β’ (πΈ β Fin β (πΈ βΎ πΌ) β Fin) |
11 | | dmfi 9280 |
. . . . . . . . . 10
β’ ((πΈ βΎ πΌ) β Fin β dom (πΈ βΎ πΌ) β Fin) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
β’ (πΈ β Fin β dom (πΈ βΎ πΌ) β Fin) |
13 | 9, 12 | eqeltrid 2838 |
. . . . . . . 8
β’ (πΈ β Fin β dom π β Fin) |
14 | 6 | fveq2i 6849 |
. . . . . . . . . 10
β’
(Vtxβπ) =
(Vtxββ¨πΎ, πβ©) |
15 | 1 | fvexi 6860 |
. . . . . . . . . . . . 13
β’ π β V |
16 | 15 | difexi 5289 |
. . . . . . . . . . . 12
β’ (π β {π}) β V |
17 | 3, 16 | eqeltri 2830 |
. . . . . . . . . . 11
β’ πΎ β V |
18 | 2 | fvexi 6860 |
. . . . . . . . . . . . 13
β’ πΈ β V |
19 | 18 | resex 5989 |
. . . . . . . . . . . 12
β’ (πΈ βΎ πΌ) β V |
20 | 5, 19 | eqeltri 2830 |
. . . . . . . . . . 11
β’ π β V |
21 | 17, 20 | opvtxfvi 28009 |
. . . . . . . . . 10
β’
(Vtxββ¨πΎ,
πβ©) = πΎ |
22 | 14, 21, 3 | 3eqtrri 2766 |
. . . . . . . . 9
β’ (π β {π}) = (Vtxβπ) |
23 | 1, 2, 3, 4, 5, 6 | vtxdginducedm1lem1 28536 |
. . . . . . . . . 10
β’
(iEdgβπ) =
π |
24 | 23 | eqcomi 2742 |
. . . . . . . . 9
β’ π = (iEdgβπ) |
25 | | eqid 2733 |
. . . . . . . . 9
β’ dom π = dom π |
26 | 22, 24, 25 | vtxdgfisnn0 28472 |
. . . . . . . 8
β’ ((dom
π β Fin β§ π£ β (π β {π})) β ((VtxDegβπ)βπ£) β
β0) |
27 | 13, 26 | sylan 581 |
. . . . . . 7
β’ ((πΈ β Fin β§ π£ β (π β {π})) β ((VtxDegβπ)βπ£) β
β0) |
28 | 27 | nn0red 12482 |
. . . . . 6
β’ ((πΈ β Fin β§ π£ β (π β {π})) β ((VtxDegβπ)βπ£) β β) |
29 | | dmfi 9280 |
. . . . . . . . . . 11
β’ (πΈ β Fin β dom πΈ β Fin) |
30 | | rabfi 9219 |
. . . . . . . . . . 11
β’ (dom
πΈ β Fin β {π β dom πΈ β£ π β (πΈβπ)} β Fin) |
31 | 29, 30 | syl 17 |
. . . . . . . . . 10
β’ (πΈ β Fin β {π β dom πΈ β£ π β (πΈβπ)} β Fin) |
32 | 7, 31 | eqeltrid 2838 |
. . . . . . . . 9
β’ (πΈ β Fin β π½ β Fin) |
33 | | rabfi 9219 |
. . . . . . . . 9
β’ (π½ β Fin β {π β π½ β£ π£ β (πΈβπ)} β Fin) |
34 | | hashcl 14265 |
. . . . . . . . 9
β’ ({π β π½ β£ π£ β (πΈβπ)} β Fin β (β―β{π β π½ β£ π£ β (πΈβπ)}) β
β0) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . 8
β’ (πΈ β Fin β
(β―β{π β
π½ β£ π£ β (πΈβπ)}) β
β0) |
36 | 35 | adantr 482 |
. . . . . . 7
β’ ((πΈ β Fin β§ π£ β (π β {π})) β (β―β{π β π½ β£ π£ β (πΈβπ)}) β
β0) |
37 | 36 | nn0red 12482 |
. . . . . 6
β’ ((πΈ β Fin β§ π£ β (π β {π})) β (β―β{π β π½ β£ π£ β (πΈβπ)}) β β) |
38 | 28, 37 | rexaddd 13162 |
. . . . 5
β’ ((πΈ β Fin β§ π£ β (π β {π})) β (((VtxDegβπ)βπ£) +π (β―β{π β π½ β£ π£ β (πΈβπ)})) = (((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)}))) |
39 | 38 | eqeq2d 2744 |
. . . 4
β’ ((πΈ β Fin β§ π£ β (π β {π})) β (((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) +π (β―β{π β π½ β£ π£ β (πΈβπ)})) β ((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)})))) |
40 | 39 | biimpd 228 |
. . 3
β’ ((πΈ β Fin β§ π£ β (π β {π})) β (((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) +π (β―β{π β π½ β£ π£ β (πΈβπ)})) β ((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)})))) |
41 | 40 | ralimdva 3161 |
. 2
β’ (πΈ β Fin β
(βπ£ β (π β {π})((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) +π (β―β{π β π½ β£ π£ β (πΈβπ)})) β βπ£ β (π β {π})((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)})))) |
42 | 8, 41 | mpi 20 |
1
β’ (πΈ β Fin β βπ£ β (π β {π})((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)}))) |