Metamath Proof Explorer

Theorem rusgrpropedg

Description: The properties of a k-regular simple graph expressed with edges. (Contributed by AV, 23-Dec-2020) (Revised by AV, 27-Dec-2020)

Ref Expression
Hypothesis rusgrpropnb.v 
|- V = ( Vtx ` G )
Assertion rusgrpropedg 
|- ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` { e e. ( Edg ` G ) | v e. e } ) = 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 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 1 3 nbedgusgr 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( # ` ( G NeighbVtx v ) ) = ( # ` { e e. ( Edg ` G ) | v e. e } ) )
5 4 eqeq1d 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( ( # ` ( G NeighbVtx v ) ) = K <-> ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) )
6 5 biimpd 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( ( # ` ( G NeighbVtx v ) ) = K -> ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) )
7 6 ralimdva 
 |-  ( G e. USGraph -> ( A. v e. V ( # ` ( G NeighbVtx v ) ) = K -> A. v e. V ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) )
8 7 adantr 
 |-  ( ( G e. USGraph /\ K e. NN0* ) -> ( A. v e. V ( # ` ( G NeighbVtx v ) ) = K -> A. v e. V ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) )
9 8 imdistani 
 |-  ( ( ( G e. USGraph /\ K e. NN0* ) /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) -> ( ( G e. USGraph /\ K e. NN0* ) /\ A. v e. V ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) )
10 df-3an 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) <-> ( ( G e. USGraph /\ K e. NN0* ) /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) )
11 df-3an 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) <-> ( ( G e. USGraph /\ K e. NN0* ) /\ A. v e. V ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) )
12 9 10 11 3imtr4i 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` ( G NeighbVtx v ) ) = K ) -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) )
13 2 12 syl 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( # ` { e e. ( Edg ` G ) | v e. e } ) = K ) )