Metamath Proof Explorer


Theorem rusgrpropnb

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

Ref Expression
Hypothesis rusgrpropnb.v V=VtxG
Assertion rusgrpropnb GRegUSGraphKGUSGraphK0*vVGNeighbVtxv=K

Proof

Step Hyp Ref Expression
1 rusgrpropnb.v V=VtxG
2 eqid VtxDegG=VtxDegG
3 1 2 rusgrprop0 GRegUSGraphKGUSGraphK0*vVVtxDegGv=K
4 simp1 GUSGraphK0*vVVtxDegGv=KGUSGraph
5 simp2 GUSGraphK0*vVVtxDegGv=KK0*
6 1 hashnbusgrvd GUSGraphvVGNeighbVtxv=VtxDegGv
7 6 adantlr GUSGraphK0*vVGNeighbVtxv=VtxDegGv
8 eqeq2 K=VtxDegGvGNeighbVtxv=KGNeighbVtxv=VtxDegGv
9 8 eqcoms VtxDegGv=KGNeighbVtxv=KGNeighbVtxv=VtxDegGv
10 7 9 syl5ibrcom GUSGraphK0*vVVtxDegGv=KGNeighbVtxv=K
11 10 ralimdva GUSGraphK0*vVVtxDegGv=KvVGNeighbVtxv=K
12 11 3impia GUSGraphK0*vVVtxDegGv=KvVGNeighbVtxv=K
13 4 5 12 3jca GUSGraphK0*vVVtxDegGv=KGUSGraphK0*vVGNeighbVtxv=K
14 3 13 syl GRegUSGraphKGUSGraphK0*vVGNeighbVtxv=K