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

Proof

Step Hyp Ref Expression
1 rusgrpropnb.v ⊢V=Vtx⁡G
2 1 rusgrpropnb ⊢GRegUSGraphK→G∈USGraph∧K∈ℕ0*∧∀v∈VGNeighbVtxv=K
3 eqid ⊢Edg⁡G=Edg⁡G
4 1 3 nbedgusgr ⊢G∈USGraph∧v∈V→GNeighbVtxv=e∈Edg⁡G|v∈e
5 4 eqeq1d ⊢G∈USGraph∧v∈V→GNeighbVtxv=K↔e∈Edg⁡G|v∈e=K
6 5 biimpd ⊢G∈USGraph∧v∈V→GNeighbVtxv=K→e∈Edg⁡G|v∈e=K
7 6 ralimdva ⊢G∈USGraph→∀v∈VGNeighbVtxv=K→∀v∈Ve∈Edg⁡G|v∈e=K
8 7 adantr ⊢G∈USGraph∧K∈ℕ0*→∀v∈VGNeighbVtxv=K→∀v∈Ve∈Edg⁡G|v∈e=K
9 8 imdistani ⊢G∈USGraph∧K∈ℕ0*∧∀v∈VGNeighbVtxv=K→G∈USGraph∧K∈ℕ0*∧∀v∈Ve∈Edg⁡G|v∈e=K
10 df-3an ⊢G∈USGraph∧K∈ℕ0*∧∀v∈VGNeighbVtxv=K↔G∈USGraph∧K∈ℕ0*∧∀v∈VGNeighbVtxv=K
11 df-3an ⊢G∈USGraph∧K∈ℕ0*∧∀v∈Ve∈Edg⁡G|v∈e=K↔G∈USGraph∧K∈ℕ0*∧∀v∈Ve∈Edg⁡G|v∈e=K
12 9 10 11 3imtr4i ⊢G∈USGraph∧K∈ℕ0*∧∀v∈VGNeighbVtxv=K→G∈USGraph∧K∈ℕ0*∧∀v∈Ve∈Edg⁡G|v∈e=K
13 2 12 syl ⊢GRegUSGraphK→G∈USGraph∧K∈ℕ0*∧∀v∈Ve∈Edg⁡G|v∈e=K