Theorem rusgrpropedg

Description: The properties of a k-regular simple graph expressed with edges. (Contributed by AV, 23-Dec-2020) (Revised by AV, 27-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rusgrpropnb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	rusgrpropnb	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) )
3		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4	1 3	nbedgusgr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) )
5	4	eqeq1d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ↔ ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) )
6	5	biimpd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 → ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) )
7	6	ralimdva	⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) )
8	7	adantr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ) → ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) )
9	8	imdistani	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) )
10		df-3an	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) ↔ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) )
11		df-3an	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) ↔ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) )
12	9 10 11	3imtr4i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = 𝐾 ) → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) )
13	2 12	syl	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑣 ∈ 𝑒 } ) = 𝐾 ) )