Metamath Proof Explorer

Theorem rusgrpropedg

Description: The properties of a k-regular simple graph expressed with edges. (Contributed by AV, 23-Dec-2020) (Revised by AV, 27-Dec-2020)

Ref Expression
Hypothesis rusgrpropnb.v ⊢ V = Vtx ⁡ G
Assertion rusgrpropedg ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V e ∈ Edg ⁡ G | v ∈ e = 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 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 1 3 nbedgusgr ⊢ G ∈ USGraph ∧ v ∈ V → G NeighbVtx v = e ∈ Edg ⁡ G | v ∈ e
5 4 eqeq1d ⊢ G ∈ USGraph ∧ v ∈ V → G NeighbVtx v = K ↔ e ∈ Edg ⁡ G | v ∈ e = K
6 5 biimpd ⊢ G ∈ USGraph ∧ v ∈ V → G NeighbVtx v = K → e ∈ Edg ⁡ G | v ∈ e = K
7 6 ralimdva ⊢ G ∈ USGraph → ∀ v ∈ V G NeighbVtx v = K → ∀ v ∈ V e ∈ Edg ⁡ G | v ∈ e = K
8 7 adantr ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * → ∀ v ∈ V G NeighbVtx v = K → ∀ v ∈ V e ∈ Edg ⁡ G | v ∈ e = K
9 8 imdistani ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V e ∈ Edg ⁡ G | v ∈ e = K
10 df-3an ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K ↔ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K
11 df-3an ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V e ∈ Edg ⁡ G | v ∈ e = K ↔ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V e ∈ Edg ⁡ G | v ∈ e = K
12 9 10 11 3imtr4i ⊢ G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V G NeighbVtx v = K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V e ∈ Edg ⁡ G | v ∈ e = K
13 2 12 syl ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V e ∈ Edg ⁡ G | v ∈ e = K