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 ⊢GRegUSGraphK→G∈USGraph∧K∈ℕ0*∧∀v∈Vk∈V|vk∈Edg⁡G=K

Proof

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