Step | Hyp | Ref
| Expression |
1 | | fusgreghash2wsp.v |
. . . . . 6
β’ π = (VtxβπΊ) |
2 | | fveq1 6841 |
. . . . . . . . 9
β’ (π = π‘ β (π β1) = (π‘β1)) |
3 | 2 | eqeq1d 2738 |
. . . . . . . 8
β’ (π = π‘ β ((π β1) = π β (π‘β1) = π)) |
4 | 3 | cbvrabv 3417 |
. . . . . . 7
β’ {π β (2 WSPathsN πΊ) β£ (π β1) = π} = {π‘ β (2 WSPathsN πΊ) β£ (π‘β1) = π} |
5 | 4 | mpteq2i 5210 |
. . . . . 6
β’ (π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π}) = (π β π β¦ {π‘ β (2 WSPathsN πΊ) β£ (π‘β1) = π}) |
6 | 1, 5 | fusgreg2wsp 29280 |
. . . . 5
β’ (πΊ β FinUSGraph β (2
WSPathsN πΊ) = βͺ π¦ β π ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) |
7 | 6 | ad2antrr 724 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (2 WSPathsN πΊ) = βͺ
π¦ β π ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) |
8 | 7 | fveq2d 6846 |
. . 3
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (β―β(2 WSPathsN πΊ)) = (β―ββͺ π¦ β π ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦))) |
9 | 1 | fusgrvtxfi 28267 |
. . . . 5
β’ (πΊ β FinUSGraph β π β Fin) |
10 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π = π¦ β ((π β1) = π β (π β1) = π¦)) |
11 | 10 | rabbidv 3415 |
. . . . . . . 8
β’ (π = π¦ β {π β (2 WSPathsN πΊ) β£ (π β1) = π} = {π β (2 WSPathsN πΊ) β£ (π β1) = π¦}) |
12 | | eqid 2736 |
. . . . . . . 8
β’ (π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π}) = (π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π}) |
13 | | ovex 7390 |
. . . . . . . . 9
β’ (2
WSPathsN πΊ) β
V |
14 | 13 | rabex 5289 |
. . . . . . . 8
β’ {π β (2 WSPathsN πΊ) β£ (π β1) = π¦} β V |
15 | 11, 12, 14 | fvmpt 6948 |
. . . . . . 7
β’ (π¦ β π β ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦) = {π β (2 WSPathsN πΊ) β£ (π β1) = π¦}) |
16 | 15 | adantl 482 |
. . . . . 6
β’ ((πΊ β FinUSGraph β§ π¦ β π) β ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦) = {π β (2 WSPathsN πΊ) β£ (π β1) = π¦}) |
17 | | eqid 2736 |
. . . . . . . . 9
β’
(VtxβπΊ) =
(VtxβπΊ) |
18 | 17 | fusgrvtxfi 28267 |
. . . . . . . 8
β’ (πΊ β FinUSGraph β
(VtxβπΊ) β
Fin) |
19 | | wspthnfi 28864 |
. . . . . . . 8
β’
((VtxβπΊ)
β Fin β (2 WSPathsN πΊ) β Fin) |
20 | | rabfi 9213 |
. . . . . . . 8
β’ ((2
WSPathsN πΊ) β Fin
β {π β (2
WSPathsN πΊ) β£ (π β1) = π¦} β Fin) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . 7
β’ (πΊ β FinUSGraph β {π β (2 WSPathsN πΊ) β£ (π β1) = π¦} β Fin) |
22 | 21 | adantr 481 |
. . . . . 6
β’ ((πΊ β FinUSGraph β§ π¦ β π) β {π β (2 WSPathsN πΊ) β£ (π β1) = π¦} β Fin) |
23 | 16, 22 | eqeltrd 2837 |
. . . . 5
β’ ((πΊ β FinUSGraph β§ π¦ β π) β ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦) β Fin) |
24 | 1, 5 | 2wspmdisj 29281 |
. . . . . 6
β’
Disj π¦ β
π ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦) |
25 | 24 | a1i 11 |
. . . . 5
β’ (πΊ β FinUSGraph β
Disj π¦ β π ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) |
26 | 9, 23, 25 | hashiun 15707 |
. . . 4
β’ (πΊ β FinUSGraph β
(β―ββͺ π¦ β π ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) = Ξ£π¦ β π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦))) |
27 | 26 | ad2antrr 724 |
. . 3
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (β―ββͺ π¦ β π ((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) = Ξ£π¦ β π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦))) |
28 | 1, 5 | fusgreghash2wspv 29279 |
. . . . . . . . 9
β’ (πΊ β FinUSGraph β
βπ£ β π (((VtxDegβπΊ)βπ£) = πΎ β (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (πΎ Β· (πΎ β 1)))) |
29 | | ralim 3089 |
. . . . . . . . 9
β’
(βπ£ β
π (((VtxDegβπΊ)βπ£) = πΎ β (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (πΎ Β· (πΎ β 1))) β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β βπ£ β π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (πΎ Β· (πΎ β 1)))) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
β’ (πΊ β FinUSGraph β
(βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β βπ£ β π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (πΎ Β· (πΎ β 1)))) |
31 | 30 | adantr 481 |
. . . . . . 7
β’ ((πΊ β FinUSGraph β§ π β β
) β
(βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β βπ£ β π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (πΎ Β· (πΎ β 1)))) |
32 | 31 | imp 407 |
. . . . . 6
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β βπ£ β π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (πΎ Β· (πΎ β 1))) |
33 | | 2fveq3 6847 |
. . . . . . . 8
β’ (π£ = π¦ β (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦))) |
34 | 33 | eqeq1d 2738 |
. . . . . . 7
β’ (π£ = π¦ β ((β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (πΎ Β· (πΎ β 1)) β (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) = (πΎ Β· (πΎ β 1)))) |
35 | 34 | rspccva 3580 |
. . . . . 6
β’
((βπ£ β
π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ£)) = (πΎ Β· (πΎ β 1)) β§ π¦ β π) β (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) = (πΎ Β· (πΎ β 1))) |
36 | 32, 35 | sylan 580 |
. . . . 5
β’ ((((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β§ π¦ β π) β (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) = (πΎ Β· (πΎ β 1))) |
37 | 36 | sumeq2dv 15588 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β Ξ£π¦ β π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) = Ξ£π¦ β π (πΎ Β· (πΎ β 1))) |
38 | 9 | adantr 481 |
. . . . 5
β’ ((πΊ β FinUSGraph β§ π β β
) β π β Fin) |
39 | | eqid 2736 |
. . . . . . . . 9
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
40 | 1, 39 | fusgrregdegfi 28517 |
. . . . . . . 8
β’ ((πΊ β FinUSGraph β§ π β β
) β
(βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β πΎ β
β0)) |
41 | 40 | imp 407 |
. . . . . . 7
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β πΎ β
β0) |
42 | 41 | nn0cnd 12475 |
. . . . . 6
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β πΎ β β) |
43 | | kcnktkm1cn 11586 |
. . . . . 6
β’ (πΎ β β β (πΎ Β· (πΎ β 1)) β
β) |
44 | 42, 43 | syl 17 |
. . . . 5
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (πΎ Β· (πΎ β 1)) β
β) |
45 | | fsumconst 15675 |
. . . . 5
β’ ((π β Fin β§ (πΎ Β· (πΎ β 1)) β β) β
Ξ£π¦ β π (πΎ Β· (πΎ β 1)) = ((β―βπ) Β· (πΎ Β· (πΎ β 1)))) |
46 | 38, 44, 45 | syl2an2r 683 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β Ξ£π¦ β π (πΎ Β· (πΎ β 1)) = ((β―βπ) Β· (πΎ Β· (πΎ β 1)))) |
47 | 37, 46 | eqtrd 2776 |
. . 3
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β Ξ£π¦ β π (β―β((π β π β¦ {π β (2 WSPathsN πΊ) β£ (π β1) = π})βπ¦)) = ((β―βπ) Β· (πΎ Β· (πΎ β 1)))) |
48 | 8, 27, 47 | 3eqtrd 2780 |
. 2
β’ (((πΊ β FinUSGraph β§ π β β
) β§
βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (β―β(2 WSPathsN πΊ)) = ((β―βπ) Β· (πΎ Β· (πΎ β 1)))) |
49 | 48 | ex 413 |
1
β’ ((πΊ β FinUSGraph β§ π β β
) β
(βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (β―β(2 WSPathsN πΊ)) = ((β―βπ) Β· (πΎ Β· (πΎ β 1))))) |