Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | | 1egrvtxdg1.a |
. . . 4
β’ (π β π΄ β π) |
3 | | 1egrvtxdg1.b |
. . . . 5
β’ (π β π΅ β π) |
4 | | 1egrvtxdg1.v |
. . . . 5
β’ (π β (VtxβπΊ) = π) |
5 | 3, 4 | eleqtrrd 2837 |
. . . 4
β’ (π β π΅ β (VtxβπΊ)) |
6 | | 1egrvtxdg1.c |
. . . . 5
β’ (π β πΆ β π) |
7 | 6, 4 | eleqtrrd 2837 |
. . . 4
β’ (π β πΆ β (VtxβπΊ)) |
8 | | 1egrvtxdg1.i |
. . . 4
β’ (π β (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) |
9 | | 1egrvtxdg1.n |
. . . 4
β’ (π β π΅ β πΆ) |
10 | 1, 2, 5, 7, 8, 9 | usgr1e 28235 |
. . 3
β’ (π β πΊ β USGraph) |
11 | | eqid 2733 |
. . . 4
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
12 | | eqid 2733 |
. . . 4
β’ dom
(iEdgβπΊ) = dom
(iEdgβπΊ) |
13 | | eqid 2733 |
. . . 4
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
14 | 1, 11, 12, 13 | vtxdusgrval 28477 |
. . 3
β’ ((πΊ β USGraph β§ π΅ β (VtxβπΊ)) β ((VtxDegβπΊ)βπ΅) = (β―β{π₯ β dom (iEdgβπΊ) β£ π΅ β ((iEdgβπΊ)βπ₯)})) |
15 | 10, 5, 14 | syl2anc 585 |
. 2
β’ (π β ((VtxDegβπΊ)βπ΅) = (β―β{π₯ β dom (iEdgβπΊ) β£ π΅ β ((iEdgβπΊ)βπ₯)})) |
16 | | dmeq 5860 |
. . . . . . . 8
β’
((iEdgβπΊ) =
{β¨π΄, {π΅, πΆ}β©} β dom (iEdgβπΊ) = dom {β¨π΄, {π΅, πΆ}β©}) |
17 | 16 | adantl 483 |
. . . . . . 7
β’ ((π β§ (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β dom (iEdgβπΊ) = dom {β¨π΄, {π΅, πΆ}β©}) |
18 | | prex 5390 |
. . . . . . . 8
β’ {π΅, πΆ} β V |
19 | | dmsnopg 6166 |
. . . . . . . 8
β’ ({π΅, πΆ} β V β dom {β¨π΄, {π΅, πΆ}β©} = {π΄}) |
20 | 18, 19 | mp1i 13 |
. . . . . . 7
β’ ((π β§ (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β dom {β¨π΄, {π΅, πΆ}β©} = {π΄}) |
21 | 17, 20 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β dom (iEdgβπΊ) = {π΄}) |
22 | | fveq1 6842 |
. . . . . . . 8
β’
((iEdgβπΊ) =
{β¨π΄, {π΅, πΆ}β©} β ((iEdgβπΊ)βπ₯) = ({β¨π΄, {π΅, πΆ}β©}βπ₯)) |
23 | 22 | eleq2d 2820 |
. . . . . . 7
β’
((iEdgβπΊ) =
{β¨π΄, {π΅, πΆ}β©} β (π΅ β ((iEdgβπΊ)βπ₯) β π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯))) |
24 | 23 | adantl 483 |
. . . . . 6
β’ ((π β§ (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β (π΅ β ((iEdgβπΊ)βπ₯) β π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯))) |
25 | 21, 24 | rabeqbidv 3423 |
. . . . 5
β’ ((π β§ (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β {π₯ β dom (iEdgβπΊ) β£ π΅ β ((iEdgβπΊ)βπ₯)} = {π₯ β {π΄} β£ π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯)}) |
26 | 25 | fveq2d 6847 |
. . . 4
β’ ((π β§ (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β (β―β{π₯ β dom (iEdgβπΊ) β£ π΅ β ((iEdgβπΊ)βπ₯)}) = (β―β{π₯ β {π΄} β£ π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯)})) |
27 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π₯ = π΄ β ({β¨π΄, {π΅, πΆ}β©}βπ₯) = ({β¨π΄, {π΅, πΆ}β©}βπ΄)) |
28 | 27 | eleq2d 2820 |
. . . . . . . . 9
β’ (π₯ = π΄ β (π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯) β π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ΄))) |
29 | 28 | rabsnif 4685 |
. . . . . . . 8
β’ {π₯ β {π΄} β£ π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯)} = if(π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ΄), {π΄}, β
) |
30 | | prid1g 4722 |
. . . . . . . . . . 11
β’ (π΅ β π β π΅ β {π΅, πΆ}) |
31 | 3, 30 | syl 17 |
. . . . . . . . . 10
β’ (π β π΅ β {π΅, πΆ}) |
32 | | fvsng 7127 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ {π΅, πΆ} β V) β ({β¨π΄, {π΅, πΆ}β©}βπ΄) = {π΅, πΆ}) |
33 | 2, 18, 32 | sylancl 587 |
. . . . . . . . . 10
β’ (π β ({β¨π΄, {π΅, πΆ}β©}βπ΄) = {π΅, πΆ}) |
34 | 31, 33 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (π β π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ΄)) |
35 | 34 | iftrued 4495 |
. . . . . . . 8
β’ (π β if(π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ΄), {π΄}, β
) = {π΄}) |
36 | 29, 35 | eqtrid 2785 |
. . . . . . 7
β’ (π β {π₯ β {π΄} β£ π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯)} = {π΄}) |
37 | 36 | fveq2d 6847 |
. . . . . 6
β’ (π β (β―β{π₯ β {π΄} β£ π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯)}) = (β―β{π΄})) |
38 | | hashsng 14275 |
. . . . . . 7
β’ (π΄ β π β (β―β{π΄}) = 1) |
39 | 2, 38 | syl 17 |
. . . . . 6
β’ (π β (β―β{π΄}) = 1) |
40 | 37, 39 | eqtrd 2773 |
. . . . 5
β’ (π β (β―β{π₯ β {π΄} β£ π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯)}) = 1) |
41 | 40 | adantr 482 |
. . . 4
β’ ((π β§ (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β (β―β{π₯ β {π΄} β£ π΅ β ({β¨π΄, {π΅, πΆ}β©}βπ₯)}) = 1) |
42 | 26, 41 | eqtrd 2773 |
. . 3
β’ ((π β§ (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β (β―β{π₯ β dom (iEdgβπΊ) β£ π΅ β ((iEdgβπΊ)βπ₯)}) = 1) |
43 | 8, 42 | mpdan 686 |
. 2
β’ (π β (β―β{π₯ β dom (iEdgβπΊ) β£ π΅ β ((iEdgβπΊ)βπ₯)}) = 1) |
44 | 15, 43 | eqtrd 2773 |
1
β’ (π β ((VtxDegβπΊ)βπ΅) = 1) |