Description: The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018) (Revised by AV, 26-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isrgr.v | |- V = ( Vtx ` G ) |
|
isrgr.d | |- D = ( VtxDeg ` G ) |
||
Assertion | rgrprop | |- ( G RegGraph K -> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isrgr.v | |- V = ( Vtx ` G ) |
|
2 | isrgr.d | |- D = ( VtxDeg ` G ) |
|
3 | df-rgr | |- RegGraph = { <. g , k >. | ( k e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k ) } |
|
4 | 3 | bropaex12 | |- ( G RegGraph K -> ( G e. _V /\ K e. _V ) ) |
5 | 1 2 | isrgr | |- ( ( G e. _V /\ K e. _V ) -> ( G RegGraph K <-> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) ) |
6 | 5 | biimpd | |- ( ( G e. _V /\ K e. _V ) -> ( G RegGraph K -> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) ) |
7 | 4 6 | mpcom | |- ( G RegGraph K -> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) |