Metamath Proof Explorer

Theorem rusgrpropnb

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

Ref Expression
Hypothesis rusgrpropnb.v ⊢ V = Vtx ⁡ G
Assertion rusgrpropnb ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K

Proof

Step Hyp Ref Expression
1 rusgrpropnb.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
3 1 2 rusgrprop0 ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K
4 simp1 ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → G ∈ USGraph
5 simp2 ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℕ 0 *
6 1 hashnbusgrvd ⊢ G ∈ USGraph ∧ v ∈ V → G NeighbVtx v = VtxDeg ⁡ G ⁡ v
7 6 adantlr ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ v ∈ V → G NeighbVtx v = VtxDeg ⁡ G ⁡ v
8 eqeq2 ⊢ K = VtxDeg ⁡ G ⁡ v → G NeighbVtx v = K ↔ G NeighbVtx v = VtxDeg ⁡ G ⁡ v
9 8 eqcoms ⊢ VtxDeg ⁡ G ⁡ v = K → G NeighbVtx v = K ↔ G NeighbVtx v = VtxDeg ⁡ G ⁡ v
10 7 9 syl5ibrcom ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ v ∈ V → VtxDeg ⁡ G ⁡ v = K → G NeighbVtx v = K
11 10 ralimdva ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → ∀ v ∈ V G NeighbVtx v = K
12 11 3impia ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → ∀ v ∈ V G NeighbVtx v = K
13 4 5 12 3jca ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K
14 3 13 syl ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K