Metamath Proof Explorer

Theorem fusgrn0eqdrusgr

Description: If all vertices in a nonempty finite simple graph have the same (finite) degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020)

Ref Expression
Hypotheses isrusgr0.v 
|- V = ( Vtx ` G )
isrusgr0.d 
|- D = ( VtxDeg ` G )
Assertion fusgrn0eqdrusgr 
|- ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( D ` v ) = K -> G RegUSGraph K ) )

Proof

Step Hyp Ref Expression
1 isrusgr0.v 
 |-  V = ( Vtx ` G )
2 isrusgr0.d 
 |-  D = ( VtxDeg ` G )
3 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
4 3 ad2antrr 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( D ` v ) = K ) -> G e. USGraph )
5 1 2 fusgrregdegfi 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( D ` v ) = K -> K e. NN0 ) )
6 5 imp 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( D ` v ) = K ) -> K e. NN0 )
7 6 nn0xnn0d 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( D ` v ) = K ) -> K e. NN0* )
8 simpr 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( D ` v ) = K ) -> A. v e. V ( D ` v ) = K )
9 1 2 usgreqdrusgr 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) -> G RegUSGraph K )
10 4 7 8 9 syl3anc 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( D ` v ) = K ) -> G RegUSGraph K )
11 10 ex 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( D ` v ) = K -> G RegUSGraph K ) )