Metamath Proof Explorer

Theorem rusgrpropadjvtx

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

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

Proof

Step Hyp Ref Expression
1 rusgrpropnb.v ⊢ V = Vtx ⁡ G
2 1 rusgrpropnb ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K
3 simp1 ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K → G ∈ USGraph
4 simp2 ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K → K ∈ ℕ 0 *
5 eqid ⊢ Edg ⁡ G = Edg ⁡ G
6 1 5 nbusgrvtx ⊢ G ∈ USGraph ∧ v ∈ V → G NeighbVtx v = k ∈ V | v k ∈ Edg ⁡ G
7 6 fveq2d ⊢ G ∈ USGraph ∧ v ∈ V → G NeighbVtx v = k ∈ V | v k ∈ Edg ⁡ G
8 7 eqcomd ⊢ G ∈ USGraph ∧ v ∈ V → k ∈ V | v k ∈ Edg ⁡ G = G NeighbVtx v
9 8 adantr ⊢ G ∈ USGraph ∧ v ∈ V ∧ G NeighbVtx v = K → k ∈ V | v k ∈ Edg ⁡ G = G NeighbVtx v
10 simpr ⊢ G ∈ USGraph ∧ v ∈ V ∧ G NeighbVtx v = K → G NeighbVtx v = K
11 9 10 eqtrd ⊢ G ∈ USGraph ∧ v ∈ V ∧ G NeighbVtx v = K → k ∈ V | v k ∈ Edg ⁡ G = K
12 11 ex ⊢ G ∈ USGraph ∧ v ∈ V → G NeighbVtx v = K → k ∈ V | v k ∈ Edg ⁡ G = K
13 12 ralimdva ⊢ G ∈ USGraph → ∀ v ∈ V G NeighbVtx v = K → ∀ v ∈ V k ∈ V | v k ∈ Edg ⁡ G = K
14 13 imp ⊢ G ∈ USGraph ∧ ∀ v ∈ V G NeighbVtx v = K → ∀ v ∈ V k ∈ V | v k ∈ Edg ⁡ G = K
15 14 3adant2 ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K → ∀ v ∈ V k ∈ V | v k ∈ Edg ⁡ G = K
16 3 4 15 3jca ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V k ∈ V | v k ∈ Edg ⁡ G = K
17 2 16 syl ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V k ∈ V | v k ∈ Edg ⁡ G = K