Metamath Proof Explorer


Theorem rusgrprop0

Description: The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Hypotheses isrusgr0.v V=VtxG
isrusgr0.d D=VtxDegG
Assertion rusgrprop0 GRegUSGraphKGUSGraphK0*vVDv=K

Proof

Step Hyp Ref Expression
1 isrusgr0.v V=VtxG
2 isrusgr0.d D=VtxDegG
3 rusgrprop GRegUSGraphKGUSGraphGRegGraphK
4 1 2 rgrprop GRegGraphKK0*vVDv=K
5 4 anim2i GUSGraphGRegGraphKGUSGraphK0*vVDv=K
6 3anass GUSGraphK0*vVDv=KGUSGraphK0*vVDv=K
7 5 6 sylibr GUSGraphGRegGraphKGUSGraphK0*vVDv=K
8 3 7 syl GRegUSGraphKGUSGraphK0*vVDv=K