usgreqdrusgr

Description: If all vertices in a simple graph have the same 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	usgreqdrusgr	$⊢ (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K) \to G RegUSGraph K$

Step	Hyp	Ref	Expression
1		isrusgr0.v	$⊢ V = Vtx (G)$
2		isrusgr0.d	$⊢ D = VtxDeg (G)$
3	1 2	isrusgr0	$⊢ (G \in USGraph \land K \in ℕ_{0}^{}) \to (G RegUSGraph K \leftrightarrow (G \in USGraph \land K \in ℕ_{0}^{} \land \forall v \in V D (v) = K))$
4	3	3adant3	$⊢ (G \in USGraph \land K \in ℕ_{0}^{} \land \forall v \in V D (v) = K) \to (G RegUSGraph K \leftrightarrow (G \in USGraph \land K \in ℕ_{0}^{} \land \forall v \in V D (v) = K))$
5	4	ibir	$⊢ (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K) \to G RegUSGraph K$

Metamath Proof Explorer