Step | Hyp | Ref
| Expression |
1 | | 1loopgruspgr.v |
. . . . 5
β’ (π β (VtxβπΊ) = π) |
2 | | 1loopgruspgr.a |
. . . . 5
β’ (π β π΄ β π) |
3 | | 1loopgruspgr.n |
. . . . 5
β’ (π β π β π) |
4 | | 1loopgruspgr.i |
. . . . 5
β’ (π β (iEdgβπΊ) = {β¨π΄, {π}β©}) |
5 | 1, 2, 3, 4 | 1loopgruspgr 28490 |
. . . 4
β’ (π β πΊ β USPGraph) |
6 | | uspgrushgr 28168 |
. . . 4
β’ (πΊ β USPGraph β πΊ β
USHGraph) |
7 | 5, 6 | syl 17 |
. . 3
β’ (π β πΊ β USHGraph) |
8 | 3, 1 | eleqtrrd 2841 |
. . 3
β’ (π β π β (VtxβπΊ)) |
9 | | eqid 2737 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
10 | | eqid 2737 |
. . . 4
β’
(EdgβπΊ) =
(EdgβπΊ) |
11 | | eqid 2737 |
. . . 4
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
12 | 9, 10, 11 | vtxdushgrfvedg 28480 |
. . 3
β’ ((πΊ β USHGraph β§ π β (VtxβπΊ)) β ((VtxDegβπΊ)βπ) = ((β―β{π β (EdgβπΊ) β£ π β π}) +π
(β―β{π β
(EdgβπΊ) β£ π = {π}}))) |
13 | 7, 8, 12 | syl2anc 585 |
. 2
β’ (π β ((VtxDegβπΊ)βπ) = ((β―β{π β (EdgβπΊ) β£ π β π}) +π
(β―β{π β
(EdgβπΊ) β£ π = {π}}))) |
14 | | snex 5393 |
. . . . . . . 8
β’ {π} β V |
15 | | sneq 4601 |
. . . . . . . . 9
β’ (π = {π} β {π} = {{π}}) |
16 | 15 | eqeq2d 2748 |
. . . . . . . 8
β’ (π = {π} β ({{π}} = {π} β {{π}} = {{π}})) |
17 | | eqid 2737 |
. . . . . . . 8
β’ {{π}} = {{π}} |
18 | 14, 16, 17 | ceqsexv2d 3500 |
. . . . . . 7
β’
βπ{{π}} = {π} |
19 | 18 | a1i 11 |
. . . . . 6
β’ (π β βπ{{π}} = {π}) |
20 | | snidg 4625 |
. . . . . . . . . 10
β’ (π β π β π β {π}) |
21 | 3, 20 | syl 17 |
. . . . . . . . 9
β’ (π β π β {π}) |
22 | 21 | iftrued 4499 |
. . . . . . . 8
β’ (π β if(π β {π}, {{π}}, β
) = {{π}}) |
23 | 22 | eqeq1d 2739 |
. . . . . . 7
β’ (π β (if(π β {π}, {{π}}, β
) = {π} β {{π}} = {π})) |
24 | 23 | exbidv 1925 |
. . . . . 6
β’ (π β (βπif(π β {π}, {{π}}, β
) = {π} β βπ{{π}} = {π})) |
25 | 19, 24 | mpbird 257 |
. . . . 5
β’ (π β βπif(π β {π}, {{π}}, β
) = {π}) |
26 | 1, 2, 3, 4 | 1loopgredg 28491 |
. . . . . . . . 9
β’ (π β (EdgβπΊ) = {{π}}) |
27 | 26 | rabeqdv 3425 |
. . . . . . . 8
β’ (π β {π β (EdgβπΊ) β£ π β π} = {π β {{π}} β£ π β π}) |
28 | | eleq2 2827 |
. . . . . . . . 9
β’ (π = {π} β (π β π β π β {π})) |
29 | 28 | rabsnif 4689 |
. . . . . . . 8
β’ {π β {{π}} β£ π β π} = if(π β {π}, {{π}}, β
) |
30 | 27, 29 | eqtrdi 2793 |
. . . . . . 7
β’ (π β {π β (EdgβπΊ) β£ π β π} = if(π β {π}, {{π}}, β
)) |
31 | 30 | eqeq1d 2739 |
. . . . . 6
β’ (π β ({π β (EdgβπΊ) β£ π β π} = {π} β if(π β {π}, {{π}}, β
) = {π})) |
32 | 31 | exbidv 1925 |
. . . . 5
β’ (π β (βπ{π β (EdgβπΊ) β£ π β π} = {π} β βπif(π β {π}, {{π}}, β
) = {π})) |
33 | 25, 32 | mpbird 257 |
. . . 4
β’ (π β βπ{π β (EdgβπΊ) β£ π β π} = {π}) |
34 | | fvex 6860 |
. . . . . 6
β’
(EdgβπΊ) β
V |
35 | 34 | rabex 5294 |
. . . . 5
β’ {π β (EdgβπΊ) β£ π β π} β V |
36 | | hash1snb 14326 |
. . . . 5
β’ ({π β (EdgβπΊ) β£ π β π} β V β ((β―β{π β (EdgβπΊ) β£ π β π}) = 1 β βπ{π β (EdgβπΊ) β£ π β π} = {π})) |
37 | 35, 36 | ax-mp 5 |
. . . 4
β’
((β―β{π
β (EdgβπΊ)
β£ π β π}) = 1 β βπ{π β (EdgβπΊ) β£ π β π} = {π}) |
38 | 33, 37 | sylibr 233 |
. . 3
β’ (π β (β―β{π β (EdgβπΊ) β£ π β π}) = 1) |
39 | | eqid 2737 |
. . . . . . . . 9
β’ {π} = {π} |
40 | 39 | iftruei 4498 |
. . . . . . . 8
β’ if({π} = {π}, {{π}}, β
) = {{π}} |
41 | 40 | eqeq1i 2742 |
. . . . . . 7
β’
(if({π} = {π}, {{π}}, β
) = {π} β {{π}} = {π}) |
42 | 41 | exbii 1851 |
. . . . . 6
β’
(βπif({π} = {π}, {{π}}, β
) = {π} β βπ{{π}} = {π}) |
43 | 19, 42 | sylibr 233 |
. . . . 5
β’ (π β βπif({π} = {π}, {{π}}, β
) = {π}) |
44 | 26 | rabeqdv 3425 |
. . . . . . . 8
β’ (π β {π β (EdgβπΊ) β£ π = {π}} = {π β {{π}} β£ π = {π}}) |
45 | | eqeq1 2741 |
. . . . . . . . 9
β’ (π = {π} β (π = {π} β {π} = {π})) |
46 | 45 | rabsnif 4689 |
. . . . . . . 8
β’ {π β {{π}} β£ π = {π}} = if({π} = {π}, {{π}}, β
) |
47 | 44, 46 | eqtrdi 2793 |
. . . . . . 7
β’ (π β {π β (EdgβπΊ) β£ π = {π}} = if({π} = {π}, {{π}}, β
)) |
48 | 47 | eqeq1d 2739 |
. . . . . 6
β’ (π β ({π β (EdgβπΊ) β£ π = {π}} = {π} β if({π} = {π}, {{π}}, β
) = {π})) |
49 | 48 | exbidv 1925 |
. . . . 5
β’ (π β (βπ{π β (EdgβπΊ) β£ π = {π}} = {π} β βπif({π} = {π}, {{π}}, β
) = {π})) |
50 | 43, 49 | mpbird 257 |
. . . 4
β’ (π β βπ{π β (EdgβπΊ) β£ π = {π}} = {π}) |
51 | 34 | rabex 5294 |
. . . . 5
β’ {π β (EdgβπΊ) β£ π = {π}} β V |
52 | | hash1snb 14326 |
. . . . 5
β’ ({π β (EdgβπΊ) β£ π = {π}} β V β ((β―β{π β (EdgβπΊ) β£ π = {π}}) = 1 β βπ{π β (EdgβπΊ) β£ π = {π}} = {π})) |
53 | 51, 52 | ax-mp 5 |
. . . 4
β’
((β―β{π
β (EdgβπΊ)
β£ π = {π}}) = 1 β βπ{π β (EdgβπΊ) β£ π = {π}} = {π}) |
54 | 50, 53 | sylibr 233 |
. . 3
β’ (π β (β―β{π β (EdgβπΊ) β£ π = {π}}) = 1) |
55 | 38, 54 | oveq12d 7380 |
. 2
β’ (π β ((β―β{π β (EdgβπΊ) β£ π β π}) +π
(β―β{π β
(EdgβπΊ) β£ π = {π}})) = (1 +π
1)) |
56 | | 1re 11162 |
. . . . 5
β’ 1 β
β |
57 | | rexadd 13158 |
. . . . 5
β’ ((1
β β β§ 1 β β) β (1 +π 1) = (1
+ 1)) |
58 | 56, 56, 57 | mp2an 691 |
. . . 4
β’ (1
+π 1) = (1 + 1) |
59 | | 1p1e2 12285 |
. . . 4
β’ (1 + 1) =
2 |
60 | 58, 59 | eqtri 2765 |
. . 3
β’ (1
+π 1) = 2 |
61 | 60 | a1i 11 |
. 2
β’ (π β (1 +π
1) = 2) |
62 | 13, 55, 61 | 3eqtrd 2781 |
1
β’ (π β ((VtxDegβπΊ)βπ) = 2) |