Metamath Proof Explorer

Theorem isrgr

Description: The property of a class being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Hypotheses isrgr.v ⊢V=Vtx⁡G
isrgr.d ⊢D=VtxDeg⁡G
Assertion isrgr ⊢G∈W∧K∈Z→GRegGraphK↔K∈ℕ0*∧∀v∈VD⁡v=K

Proof

Step Hyp Ref Expression
1 isrgr.v ⊢V=Vtx⁡G
2 isrgr.d ⊢D=VtxDeg⁡G
3 eleq1 ⊢k=K→k∈ℕ0*↔K∈ℕ0*
4 3 adantl ⊢g=G∧k=K→k∈ℕ0*↔K∈ℕ0*
5 fveq2 ⊢g=G→Vtx⁡g=Vtx⁡G
6 5 adantr ⊢g=G∧k=K→Vtx⁡g=Vtx⁡G
7 fveq2 ⊢g=G→VtxDeg⁡g=VtxDeg⁡G
8 7 fveq1d ⊢g=G→VtxDeg⁡g⁡v=VtxDeg⁡G⁡v
9 8 adantr ⊢g=G∧k=K→VtxDeg⁡g⁡v=VtxDeg⁡G⁡v
10 simpr ⊢g=G∧k=K→k=K
11 9 10 eqeq12d ⊢g=G∧k=K→VtxDeg⁡g⁡v=k↔VtxDeg⁡G⁡v=K
12 6 11 raleqbidv ⊢g=G∧k=K→∀v∈Vtx⁡gVtxDeg⁡g⁡v=k↔∀v∈Vtx⁡GVtxDeg⁡G⁡v=K
13 4 12 anbi12d ⊢g=G∧k=K→k∈ℕ0*∧∀v∈Vtx⁡gVtxDeg⁡g⁡v=k↔K∈ℕ0*∧∀v∈Vtx⁡GVtxDeg⁡G⁡v=K
14 df-rgr ⊢RegGraph=gk|k∈ℕ0*∧∀v∈Vtx⁡gVtxDeg⁡g⁡v=k
15 13 14 brabga ⊢G∈W∧K∈Z→GRegGraphK↔K∈ℕ0*∧∀v∈Vtx⁡GVtxDeg⁡G⁡v=K
16 2 fveq1i ⊢D⁡v=VtxDeg⁡G⁡v
17 16 eqeq1i ⊢D⁡v=K↔VtxDeg⁡G⁡v=K
18 1 17 raleqbii ⊢∀v∈VD⁡v=K↔∀v∈Vtx⁡GVtxDeg⁡G⁡v=K
19 18 bicomi ⊢∀v∈Vtx⁡GVtxDeg⁡G⁡v=K↔∀v∈VD⁡v=K
20 19 a1i ⊢G∈W∧K∈Z→∀v∈Vtx⁡GVtxDeg⁡G⁡v=K↔∀v∈VD⁡v=K
21 20 anbi2d ⊢G∈W∧K∈Z→K∈ℕ0*∧∀v∈Vtx⁡GVtxDeg⁡G⁡v=K↔K∈ℕ0*∧∀v∈VD⁡v=K
22 15 21 bitrd ⊢G∈W∧K∈Z→GRegGraphK↔K∈ℕ0*∧∀v∈VD⁡v=K