Theorem fusgrn0eqdrusgr

Description: If all vertices in a nonempty finite simple graph have the same (finite) degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020)

	Ref	Expression
Hypotheses	isrusgr0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isrusgr0.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion	fusgrn0eqdrusgr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → 𝐺 RegUSGraph 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		isrusgr0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isrusgr0.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3		fusgrusgr	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
4	3	ad2antrr	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → 𝐺 ∈ USGraph )
5	1 2	fusgrregdegfi	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → 𝐾 ∈ ℕ0 ) )
6	5	imp	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → 𝐾 ∈ ℕ0 )
7	6	nn0xnn0d	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → 𝐾 ∈ ℕ0* )
8		simpr	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 )
9	1 2	usgreqdrusgr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → 𝐺 RegUSGraph 𝐾 )
10	4 7 8 9	syl3anc	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → 𝐺 RegUSGraph 𝐾 )
11	10	ex	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → 𝐺 RegUSGraph 𝐾 ) )