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 = ( Vtx ` G )
Assertion rusgrpropnb 
|- ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) )

Proof

Step Hyp Ref Expression
1 rusgrpropnb.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
3 1 2 rusgrprop0 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) )
4 simp1 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> G e. USGraph )
5 simp2 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> K e. NN0* )
6 1 hashnbusgrvd 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) )
7 6 adantlr 
 |-  ( ( ( G e. USGraph /\ K e. NN0* ) /\ v e. V ) -> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) )
8 eqeq2 
 |-  ( K = ( ( VtxDeg ` G ) ` v ) -> ( ( # ` ( G NeighbVtx v ) ) = K <-> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) ) )
9 8 eqcoms 
 |-  ( ( ( VtxDeg ` G ) ` v ) = K -> ( ( # ` ( G NeighbVtx v ) ) = K <-> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) ) )
10 7 9 syl5ibrcom 
 |-  ( ( ( G e. USGraph /\ K e. NN0* ) /\ v e. V ) -> ( ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( G NeighbVtx v ) ) = K ) )
11 10 ralimdva 
 |-  ( ( G e. USGraph /\ K e. NN0* ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) )
12 11 3impia 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> A. v e. V ( # ` ( G NeighbVtx v ) ) = K )
13 4 5 12 3jca 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) )
14 3 13 syl 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) )