Metamath Proof Explorer

Theorem 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 ∈ W ∧ K ∈ Z → G RegUSGraph K ↔ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K

Proof

Step Hyp Ref Expression
1 isrusgr0.v ⊢ V = Vtx ⁡ G
2 isrusgr0.d ⊢ D = VtxDeg ⁡ G
3 isrusgr ⊢ G ∈ W ∧ K ∈ Z → G RegUSGraph K ↔ G ∈ USGraph ∧ G RegGraph K
4 1 2 isrgr ⊢ G ∈ W ∧ K ∈ Z → G RegGraph K ↔ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K
5 4 anbi2d ⊢ G ∈ W ∧ K ∈ Z → G ∈ USGraph ∧ G RegGraph K ↔ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K
6 3anass ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K ↔ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K
7 5 6 bitr4di ⊢ G ∈ W ∧ K ∈ Z → G ∈ USGraph ∧ G RegGraph K ↔ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K
8 3 7 bitrd ⊢ G ∈ W ∧ K ∈ Z → G RegUSGraph K ↔ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K