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 \in FinUSGraph \land V \neq \emptyset) \to (\forall v \in V D (v) = K \to G RegUSGraph K)$

Proof

Step	Hyp	Ref	Expression
1		isrusgr0.v	$⊢ V = Vtx (G)$
2		isrusgr0.d	$⊢ D = VtxDeg (G)$
3		fusgrusgr	$⊢ G \in FinUSGraph \to G \in USGraph$
4	3	ad2antrr	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V D (v) = K) \to G \in USGraph$
5	1 2	fusgrregdegfi	$⊢ (G \in FinUSGraph \land V \neq \emptyset) \to (\forall v \in V D (v) = K \to K \in ℕ_{0})$
6	5	imp	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V D (v) = K) \to K \in ℕ_{0}$
7	6	nn0xnn0d	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V D (v) = K) \to K \in ℕ_{0}^{*}$
8		simpr	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V D (v) = K) \to \forall v \in V D (v) = K$
9	1 2	usgreqdrusgr	$⊢ (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K) \to G RegUSGraph K$
10	4 7 8 9	syl3anc	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V D (v) = K) \to G RegUSGraph K$
11	10	ex	$⊢ (G \in FinUSGraph \land V \neq \emptyset) \to (\forall v \in V D (v) = K \to G RegUSGraph K)$