Theorem rusgrpropadjvtx

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

	Ref	Expression
Hypothesis	rusgrpropnb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	rusgrpropadjvtx	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		rusgrpropnb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	rusgrpropnb	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) )
3		simp1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → 𝐺 ∈ USGraph )
4		simp2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → 𝐾 ∈ ℕ0* )
5		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
6	1 5	nbusgrvtx	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑣 ) = { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } )
7	6	fveq2d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) )
8	7	eqcomd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) )
9	8	adantr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) )
10		simpr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 )
11	9 10	eqtrd	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 )
12	11	ex	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 → ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
13	12	ralimdva	⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
14	13	imp	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 )
15	14	3adant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 )
16	3 4 15	3jca	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
17	2 16	syl	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑘 ∈ 𝑉 ∣ { 𝑣 , 𝑘 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )