rgrprop

Description: The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018) (Revised by AV, 26-Dec-2020)

	Ref	Expression
Hypotheses	isrgr.v	$⊢ V = Vtx (G)$
	isrgr.d	$⊢ D = VtxDeg (G)$
Assertion	rgrprop	$⊢ G RegGraph K \to (K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K)$

Step	Hyp	Ref	Expression
1		isrgr.v	$⊢ V = Vtx (G)$
2		isrgr.d	$⊢ D = VtxDeg (G)$
3		df-rgr	$⊢ RegGraph = \{⟨g, k⟩ \| (k \in ℕ_{0}^{*} \land \forall v \in Vtx (g) VtxDeg (g) (v) = k)\}$
4	3	bropaex12	$⊢ G RegGraph K \to (G \in V \land K \in V)$
5	1 2	isrgr	$⊢ (G \in V \land K \in V) \to (G RegGraph K \leftrightarrow (K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K))$
6	5	biimpd	$⊢ (G \in V \land K \in V) \to (G RegGraph K \to (K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K))$
7	4 6	mpcom	$⊢ G RegGraph K \to (K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K)$

Metamath Proof Explorer