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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isrgr.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion isrgr ( ( 𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍 ) → ( 𝐺 RegGraph 𝐾 ↔ ( 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 isrgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isrgr.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3 eleq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 ∈ ℕ0* ↔ 𝐾 ∈ ℕ0* ) )
4 3 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝐾 ) → ( 𝑘 ∈ ℕ0* ↔ 𝐾 ∈ ℕ0* ) )
5 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
6 5 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝐾 ) → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
7 fveq2 ⊢ ( 𝑔 = 𝐺 → ( VtxDeg ‘ 𝑔 ) = ( VtxDeg ‘ 𝐺 ) )
8 7 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
9 8 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝐾 ) → ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
10 simpr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝐾 ) → 𝑘 = 𝐾 )
11 9 10 eqeq12d ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝐾 ) → ( ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
12 6 11 raleqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝐾 ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
13 4 12 anbi12d ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝐾 ) → ( ( 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ) ↔ ( 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ) )
14 df-rgr ⊢ RegGraph = { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ) }
15 13 14 brabga ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍 ) → ( 𝐺 RegGraph 𝐾 ↔ ( 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ) )
16 2 fveq1i ⊢ ( 𝐷 ‘ 𝑣 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 )
17 16 eqeq1i ⊢ ( ( 𝐷 ‘ 𝑣 ) = 𝐾 ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 )
18 1 17 raleqbii ⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 )
19 18 bicomi ⊢ ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 )
20 19 a1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍 ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) )
21 20 anbi2d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍 ) → ( ( 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ↔ ( 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) ) )
22 15 21 bitrd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍 ) → ( 𝐺 RegGraph 𝐾 ↔ ( 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) ) )