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 → G RegGraph K ↔ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ 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 ⁡ g VtxDeg ⁡ g ⁡ v = k ↔ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = K
13 4 12 anbi12d ⊢ g = G ∧ k = K → k ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k ↔ K ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = K
14 df-rgr ⊢ RegGraph = g k | k ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k
15 13 14 brabga ⊢ G ∈ W ∧ K ∈ Z → G RegGraph K ↔ K ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ 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 ∈ V D ⁡ v = K ↔ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = K
19 18 bicomi ⊢ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = K ↔ ∀ v ∈ V D ⁡ v = K
20 19 a1i ⊢ G ∈ W ∧ K ∈ Z → ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = K ↔ ∀ v ∈ V D ⁡ v = K
21 20 anbi2d ⊢ G ∈ W ∧ K ∈ Z → K ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = K ↔ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K
22 15 21 bitrd ⊢ G ∈ W ∧ K ∈ Z → G RegGraph K ↔ K ∈ ℕ 0 * ∧ ∀ v ∈ V D ⁡ v = K