Step | Hyp | Ref
| Expression |
1 | | eleq1 2822 |
. . . . 5
β’ (π = πΎ β (π β β0*
β πΎ β
β0*)) |
2 | 1 | adantl 483 |
. . . 4
β’ ((π = πΊ β§ π = πΎ) β (π β β0*
β πΎ β
β0*)) |
3 | | fveq2 6892 |
. . . . . 6
β’ (π = πΊ β (Vtxβπ) = (VtxβπΊ)) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((π = πΊ β§ π = πΎ) β (Vtxβπ) = (VtxβπΊ)) |
5 | | fveq2 6892 |
. . . . . . . 8
β’ (π = πΊ β (VtxDegβπ) = (VtxDegβπΊ)) |
6 | 5 | fveq1d 6894 |
. . . . . . 7
β’ (π = πΊ β ((VtxDegβπ)βπ£) = ((VtxDegβπΊ)βπ£)) |
7 | 6 | adantr 482 |
. . . . . 6
β’ ((π = πΊ β§ π = πΎ) β ((VtxDegβπ)βπ£) = ((VtxDegβπΊ)βπ£)) |
8 | | simpr 486 |
. . . . . 6
β’ ((π = πΊ β§ π = πΎ) β π = πΎ) |
9 | 7, 8 | eqeq12d 2749 |
. . . . 5
β’ ((π = πΊ β§ π = πΎ) β (((VtxDegβπ)βπ£) = π β ((VtxDegβπΊ)βπ£) = πΎ)) |
10 | 4, 9 | raleqbidv 3343 |
. . . 4
β’ ((π = πΊ β§ π = πΎ) β (βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π β βπ£ β (VtxβπΊ)((VtxDegβπΊ)βπ£) = πΎ)) |
11 | 2, 10 | anbi12d 632 |
. . 3
β’ ((π = πΊ β§ π = πΎ) β ((π β β0* β§
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = π) β (πΎ β β0*
β§ βπ£ β
(VtxβπΊ)((VtxDegβπΊ)βπ£) = πΎ))) |
12 | | df-rgr 28814 |
. . 3
β’ RegGraph
= {β¨π, πβ© β£ (π β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π)} |
13 | 11, 12 | brabga 5535 |
. 2
β’ ((πΊ β π β§ πΎ β π) β (πΊ RegGraph πΎ β (πΎ β β0*
β§ βπ£ β
(VtxβπΊ)((VtxDegβπΊ)βπ£) = πΎ))) |
14 | | isrgr.v |
. . . . . 6
β’ π = (VtxβπΊ) |
15 | | isrgr.d |
. . . . . . . 8
β’ π· = (VtxDegβπΊ) |
16 | 15 | fveq1i 6893 |
. . . . . . 7
β’ (π·βπ£) = ((VtxDegβπΊ)βπ£) |
17 | 16 | eqeq1i 2738 |
. . . . . 6
β’ ((π·βπ£) = πΎ β ((VtxDegβπΊ)βπ£) = πΎ) |
18 | 14, 17 | raleqbii 3339 |
. . . . 5
β’
(βπ£ β
π (π·βπ£) = πΎ β βπ£ β (VtxβπΊ)((VtxDegβπΊ)βπ£) = πΎ) |
19 | 18 | bicomi 223 |
. . . 4
β’
(βπ£ β
(VtxβπΊ)((VtxDegβπΊ)βπ£) = πΎ β βπ£ β π (π·βπ£) = πΎ) |
20 | 19 | a1i 11 |
. . 3
β’ ((πΊ β π β§ πΎ β π) β (βπ£ β (VtxβπΊ)((VtxDegβπΊ)βπ£) = πΎ β βπ£ β π (π·βπ£) = πΎ)) |
21 | 20 | anbi2d 630 |
. 2
β’ ((πΊ β π β§ πΎ β π) β ((πΎ β β0*
β§ βπ£ β
(VtxβπΊ)((VtxDegβπΊ)βπ£) = πΎ) β (πΎ β β0*
β§ βπ£ β
π (π·βπ£) = πΎ))) |
22 | 13, 21 | bitrd 279 |
1
β’ ((πΊ β π β§ πΎ β π) β (πΊ RegGraph πΎ β (πΎ β β0*
β§ βπ£ β
π (π·βπ£) = πΎ))) |