Metamath Proof Explorer

Theorem rusgrprop0

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

Ref Expression
Hypotheses isrusgr0.v ⊢ V = Vtx ⁡ G
isrusgr0.d ⊢ D = VtxDeg ⁡ G
Assertion rusgrprop0 ⊢ 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 rusgrprop ⊢ G RegUSGraph K → G ∈ USGraph ∧ G RegGraph K
4 1 2 rgrprop ⊢ G RegGraph K → K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K
5 4 anim2i ⊢ 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 sylibr ⊢ G ∈ USGraph ∧ G RegGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K
8 3 7 syl ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K