isrusgr0

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

	Ref	Expression
Hypotheses	isrusgr0.v	$⊢ V = Vtx (G)$
	isrusgr0.d	$⊢ D = VtxDeg (G)$
Assertion	isrusgr0	$⊢ (G \in W \land K \in Z) \to (G RegUSGraph K \leftrightarrow (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K))$

Step	Hyp	Ref	Expression
1		isrusgr0.v	$⊢ V = Vtx (G)$
2		isrusgr0.d	$⊢ D = VtxDeg (G)$
3		isrusgr	$⊢ (G \in W \land K \in Z) \to (G RegUSGraph K \leftrightarrow (G \in USGraph \land G RegGraph K))$
4	1 2	isrgr	$⊢ (G \in W \land K \in Z) \to (G RegGraph K \leftrightarrow (K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K))$
5	4	anbi2d	$⊢ (G \in W \land K \in Z) \to ((G \in USGraph \land G RegGraph K) \leftrightarrow (G \in USGraph \land (K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K)))$
6		3anass	$⊢ (G \in USGraph \land K \in ℕ_{0}^{} \land \forall v \in V D (v) = K) \leftrightarrow (G \in USGraph \land (K \in ℕ_{0}^{} \land \forall v \in V D (v) = K))$
7	5 6	bitr4di	$⊢ (G \in W \land K \in Z) \to ((G \in USGraph \land G RegGraph K) \leftrightarrow (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K))$
8	3 7	bitrd	$⊢ (G \in W \land K \in Z) \to (G RegUSGraph K \leftrightarrow (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall v \in V D (v) = K))$

Metamath Proof Explorer