Theorem rusgrpropnb

Description: The properties of a k-regular simple graph expressed with neighbors. (Contributed by Alexander van der Vekens, 26-Jul-2018) (Revised by AV, 26-Dec-2020)

	Ref	Expression
Hypothesis	rusgrpropnb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	rusgrpropnb	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		rusgrpropnb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eqid	⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
3	1 2	rusgrprop0	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
4		simp1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → 𝐺 ∈ USGraph )
5		simp2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → 𝐾 ∈ ℕ0* )
6	1	hashnbusgrvd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
7	6	adantlr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ) ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
8		eqeq2	⊢ ( 𝐾 = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ↔ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ) )
9	8	eqcoms	⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ↔ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ) )
10	7 9	syl5ibrcom	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) )
11	10	ralimdva	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) )
12	11	3impia	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 )
13	4 5 12	3jca	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) )
14	3 13	syl	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) )