Step | Hyp | Ref
| Expression |
1 | | cusgrsizeindb0.e |
. . . . 5
β’ πΈ = (EdgβπΊ) |
2 | | edgval 28306 |
. . . . 5
β’
(EdgβπΊ) = ran
(iEdgβπΊ) |
3 | 1, 2 | eqtri 2760 |
. . . 4
β’ πΈ = ran (iEdgβπΊ) |
4 | 3 | a1i 11 |
. . 3
β’ ((πΊ β ComplUSGraph β§ π β Fin) β πΈ = ran (iEdgβπΊ)) |
5 | 4 | fveq2d 6895 |
. 2
β’ ((πΊ β ComplUSGraph β§ π β Fin) β
(β―βπΈ) =
(β―βran (iEdgβπΊ))) |
6 | | cusgrsizeindb0.v |
. . . . 5
β’ π = (VtxβπΊ) |
7 | 6 | opeq1i 4876 |
. . . 4
β’
β¨π,
(iEdgβπΊ)β© =
β¨(VtxβπΊ),
(iEdgβπΊ)β© |
8 | | cusgrop 28692 |
. . . 4
β’ (πΊ β ComplUSGraph β
β¨(VtxβπΊ),
(iEdgβπΊ)β© β
ComplUSGraph) |
9 | 7, 8 | eqeltrid 2837 |
. . 3
β’ (πΊ β ComplUSGraph β
β¨π, (iEdgβπΊ)β© β
ComplUSGraph) |
10 | | fvex 6904 |
. . . 4
β’
(iEdgβπΊ)
β V |
11 | | fvex 6904 |
. . . . 5
β’
(Edgββ¨π£,
πβ©) β
V |
12 | | rabexg 5331 |
. . . . . 6
β’
((Edgββ¨π£,
πβ©) β V β
{π β
(Edgββ¨π£, πβ©) β£ π β π} β V) |
13 | 12 | resiexd 7217 |
. . . . 5
β’
((Edgββ¨π£,
πβ©) β V β (
I βΎ {π β
(Edgββ¨π£, πβ©) β£ π β π}) β V) |
14 | 11, 13 | ax-mp 5 |
. . . 4
β’ ( I
βΎ {π β
(Edgββ¨π£, πβ©) β£ π β π}) β V |
15 | | rneq 5935 |
. . . . . 6
β’ (π = (iEdgβπΊ) β ran π = ran (iEdgβπΊ)) |
16 | 15 | fveq2d 6895 |
. . . . 5
β’ (π = (iEdgβπΊ) β (β―βran π) = (β―βran
(iEdgβπΊ))) |
17 | | fveq2 6891 |
. . . . . 6
β’ (π£ = π β (β―βπ£) = (β―βπ)) |
18 | 17 | oveq1d 7423 |
. . . . 5
β’ (π£ = π β ((β―βπ£)C2) = ((β―βπ)C2)) |
19 | 16, 18 | eqeqan12rd 2747 |
. . . 4
β’ ((π£ = π β§ π = (iEdgβπΊ)) β ((β―βran π) = ((β―βπ£)C2) β (β―βran
(iEdgβπΊ)) =
((β―βπ)C2))) |
20 | | rneq 5935 |
. . . . . 6
β’ (π = π β ran π = ran π) |
21 | 20 | fveq2d 6895 |
. . . . 5
β’ (π = π β (β―βran π) = (β―βran π)) |
22 | | fveq2 6891 |
. . . . . 6
β’ (π£ = π€ β (β―βπ£) = (β―βπ€)) |
23 | 22 | oveq1d 7423 |
. . . . 5
β’ (π£ = π€ β ((β―βπ£)C2) = ((β―βπ€)C2)) |
24 | 21, 23 | eqeqan12rd 2747 |
. . . 4
β’ ((π£ = π€ β§ π = π) β ((β―βran π) = ((β―βπ£)C2) β (β―βran
π) = ((β―βπ€)C2))) |
25 | | vex 3478 |
. . . . . . 7
β’ π£ β V |
26 | | vex 3478 |
. . . . . . 7
β’ π β V |
27 | 25, 26 | opvtxfvi 28266 |
. . . . . 6
β’
(Vtxββ¨π£,
πβ©) = π£ |
28 | 27 | eqcomi 2741 |
. . . . 5
β’ π£ = (Vtxββ¨π£, πβ©) |
29 | | eqid 2732 |
. . . . 5
β’
(Edgββ¨π£,
πβ©) =
(Edgββ¨π£, πβ©) |
30 | | eqid 2732 |
. . . . 5
β’ {π β (Edgββ¨π£, πβ©) β£ π β π} = {π β (Edgββ¨π£, πβ©) β£ π β π} |
31 | | eqid 2732 |
. . . . 5
β’
β¨(π£ β
{π}), ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})β© = β¨(π£ β {π}), ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})β© |
32 | 28, 29, 30, 31 | cusgrres 28702 |
. . . 4
β’
((β¨π£, πβ© β ComplUSGraph β§
π β π£) β β¨(π£ β {π}), ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})β© β
ComplUSGraph) |
33 | | rneq 5935 |
. . . . . . 7
β’ (π = ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π}) β ran π = ran ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})) |
34 | 33 | fveq2d 6895 |
. . . . . 6
β’ (π = ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π}) β (β―βran π) = (β―βran ( I
βΎ {π β
(Edgββ¨π£, πβ©) β£ π β π}))) |
35 | 34 | adantl 482 |
. . . . 5
β’ ((π€ = (π£ β {π}) β§ π = ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})) β (β―βran π) = (β―βran ( I
βΎ {π β
(Edgββ¨π£, πβ©) β£ π β π}))) |
36 | | fveq2 6891 |
. . . . . . 7
β’ (π€ = (π£ β {π}) β (β―βπ€) = (β―β(π£ β {π}))) |
37 | 36 | adantr 481 |
. . . . . 6
β’ ((π€ = (π£ β {π}) β§ π = ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})) β (β―βπ€) = (β―β(π£ β {π}))) |
38 | 37 | oveq1d 7423 |
. . . . 5
β’ ((π€ = (π£ β {π}) β§ π = ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})) β ((β―βπ€)C2) = ((β―β(π£ β {π}))C2)) |
39 | 35, 38 | eqeq12d 2748 |
. . . 4
β’ ((π€ = (π£ β {π}) β§ π = ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})) β ((β―βran π) = ((β―βπ€)C2) β (β―βran (
I βΎ {π β
(Edgββ¨π£, πβ©) β£ π β π})) = ((β―β(π£ β {π}))C2))) |
40 | | edgopval 28308 |
. . . . . . . . 9
β’ ((π£ β V β§ π β V) β
(Edgββ¨π£, πβ©) = ran π) |
41 | 40 | el2v 3482 |
. . . . . . . 8
β’
(Edgββ¨π£,
πβ©) = ran π |
42 | 41 | a1i 11 |
. . . . . . 7
β’
((β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = 0)
β (Edgββ¨π£,
πβ©) = ran π) |
43 | 42 | eqcomd 2738 |
. . . . . 6
β’
((β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = 0)
β ran π =
(Edgββ¨π£, πβ©)) |
44 | 43 | fveq2d 6895 |
. . . . 5
β’
((β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = 0)
β (β―βran π) = (β―β(Edgββ¨π£, πβ©))) |
45 | | cusgrusgr 28673 |
. . . . . . 7
β’
(β¨π£, πβ© β ComplUSGraph
β β¨π£, πβ© β
USGraph) |
46 | | usgruhgr 28440 |
. . . . . . 7
β’
(β¨π£, πβ© β USGraph β
β¨π£, πβ© β UHGraph) |
47 | 45, 46 | syl 17 |
. . . . . 6
β’
(β¨π£, πβ© β ComplUSGraph
β β¨π£, πβ© β
UHGraph) |
48 | 28, 29 | cusgrsizeindb0 28703 |
. . . . . 6
β’
((β¨π£, πβ© β UHGraph β§
(β―βπ£) = 0)
β (β―β(Edgββ¨π£, πβ©)) = ((β―βπ£)C2)) |
49 | 47, 48 | sylan 580 |
. . . . 5
β’
((β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = 0)
β (β―β(Edgββ¨π£, πβ©)) = ((β―βπ£)C2)) |
50 | 44, 49 | eqtrd 2772 |
. . . 4
β’
((β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = 0)
β (β―βran π) = ((β―βπ£)C2)) |
51 | | rnresi 6074 |
. . . . . . . . . 10
β’ ran ( I
βΎ {π β
(Edgββ¨π£, πβ©) β£ π β π}) = {π β (Edgββ¨π£, πβ©) β£ π β π} |
52 | 51 | fveq2i 6894 |
. . . . . . . . 9
β’
(β―βran ( I βΎ {π β (Edgββ¨π£, πβ©) β£ π β π})) = (β―β{π β (Edgββ¨π£, πβ©) β£ π β π}) |
53 | 41 | a1i 11 |
. . . . . . . . . . 11
β’ (((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β (Edgββ¨π£, πβ©) = ran π) |
54 | 53 | rabeqdv 3447 |
. . . . . . . . . 10
β’ (((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β {π β (Edgββ¨π£, πβ©) β£ π β π} = {π β ran π β£ π β π}) |
55 | 54 | fveq2d 6895 |
. . . . . . . . 9
β’ (((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β (β―β{π β (Edgββ¨π£, πβ©) β£ π β π}) = (β―β{π β ran π β£ π β π})) |
56 | 52, 55 | eqtrid 2784 |
. . . . . . . 8
β’ (((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β (β―βran ( I βΎ
{π β
(Edgββ¨π£, πβ©) β£ π β π})) = (β―β{π β ran π β£ π β π})) |
57 | 56 | eqeq1d 2734 |
. . . . . . 7
β’ (((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β ((β―βran ( I βΎ
{π β
(Edgββ¨π£, πβ©) β£ π β π})) = ((β―β(π£ β {π}))C2) β (β―β{π β ran π β£ π β π}) = ((β―β(π£ β {π}))C2))) |
58 | 57 | biimpd 228 |
. . . . . 6
β’ (((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β ((β―βran ( I βΎ
{π β
(Edgββ¨π£, πβ©) β£ π β π})) = ((β―β(π£ β {π}))C2) β (β―β{π β ran π β£ π β π}) = ((β―β(π£ β {π}))C2))) |
59 | 58 | imdistani 569 |
. . . . 5
β’ ((((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β§ (β―βran ( I βΎ
{π β
(Edgββ¨π£, πβ©) β£ π β π})) = ((β―β(π£ β {π}))C2)) β (((π¦ + 1) β β0 β§
(β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β§ (β―β{π β ran π β£ π β π}) = ((β―β(π£ β {π}))C2))) |
60 | 41 | eqcomi 2741 |
. . . . . . 7
β’ ran π = (Edgββ¨π£, πβ©) |
61 | | eqid 2732 |
. . . . . . 7
β’ {π β ran π β£ π β π} = {π β ran π β£ π β π} |
62 | 28, 60, 61 | cusgrsize2inds 28707 |
. . . . . 6
β’ ((π¦ + 1) β β0
β ((β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£) β ((β―β{π β ran π β£ π β π}) = ((β―β(π£ β {π}))C2) β (β―βran π) = ((β―βπ£)C2)))) |
63 | 62 | imp31 418 |
. . . . 5
β’ ((((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β§ (β―β{π β ran π β£ π β π}) = ((β―β(π£ β {π}))C2)) β (β―βran π) = ((β―βπ£)C2)) |
64 | 59, 63 | syl 17 |
. . . 4
β’ ((((π¦ + 1) β β0
β§ (β¨π£, πβ© β ComplUSGraph β§
(β―βπ£) = (π¦ + 1) β§ π β π£)) β§ (β―βran ( I βΎ
{π β
(Edgββ¨π£, πβ©) β£ π β π})) = ((β―β(π£ β {π}))C2)) β (β―βran π) = ((β―βπ£)C2)) |
65 | 10, 14, 19, 24, 32, 39, 50, 64 | opfi1ind 14462 |
. . 3
β’
((β¨π,
(iEdgβπΊ)β© β
ComplUSGraph β§ π β
Fin) β (β―βran (iEdgβπΊ)) = ((β―βπ)C2)) |
66 | 9, 65 | sylan 580 |
. 2
β’ ((πΊ β ComplUSGraph β§ π β Fin) β
(β―βran (iEdgβπΊ)) = ((β―βπ)C2)) |
67 | 5, 66 | eqtrd 2772 |
1
β’ ((πΊ β ComplUSGraph β§ π β Fin) β
(β―βπΈ) =
((β―βπ)C2)) |