Metamath Proof Explorer

Theorem rusgrpropadjvtx

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

Ref Expression
Hypothesis rusgrpropnb.v 
|- V = ( Vtx ` G )
Assertion rusgrpropadjvtx 
|- ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = K ) )

Proof

Step Hyp Ref Expression
1 rusgrpropnb.v 
 |-  V = ( Vtx ` G )
2 1 rusgrpropnb 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) )
3 simp1 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) -> G e. USGraph )
4 simp2 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) -> K e. NN0* )
5 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
6 1 5 nbusgrvtx 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( G NeighbVtx v ) = { k e. V | { v , k } e. ( Edg ` G ) } )
7 6 fveq2d 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( # ` ( G NeighbVtx v ) ) = ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) )
8 7 eqcomd 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = ( # ` ( G NeighbVtx v ) ) )
9 8 adantr 
 |-  ( ( ( G e. USGraph /\ v e. V ) /\ ( # ` ( G NeighbVtx v ) ) = K ) -> ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = ( # ` ( G NeighbVtx v ) ) )
10 simpr 
 |-  ( ( ( G e. USGraph /\ v e. V ) /\ ( # ` ( G NeighbVtx v ) ) = K ) -> ( # ` ( G NeighbVtx v ) ) = K )
11 9 10 eqtrd 
 |-  ( ( ( G e. USGraph /\ v e. V ) /\ ( # ` ( G NeighbVtx v ) ) = K ) -> ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = K )
12 11 ex 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( ( # ` ( G NeighbVtx v ) ) = K -> ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = K ) )
13 12 ralimdva 
 |-  ( G e. USGraph -> ( A. v e. V ( # ` ( G NeighbVtx v ) ) = K -> A. v e. V ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = K ) )
14 13 imp 
 |-  ( ( G e. USGraph /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) -> A. v e. V ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = K )
15 14 3adant2 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) -> A. v e. V ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = K )
16 3 4 15 3jca 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = K ) )
17 2 16 syl 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` { k e. V | { v , k } e. ( Edg ` G ) } ) = K ) )