Theorem usgreqdrusgr

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

	Ref	Expression
Hypotheses	isrusgr0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isrusgr0.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
Assertion	usgreqdrusgr	$$⊢\left(G\in \mathrm{USGraph}\wedge K\in {\mathbb{N}}_0^{*}\wedge \forall v\in VD\left(v\right)=K\right)\to G\mathrm{RegUSGraph}K$$

Proof

Step	Hyp	Ref	Expression
1		isrusgr0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isrusgr0.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
3	1 2	isrusgr0	$$⊢\left(G\in \mathrm{USGraph}\wedge K\in {\mathbb{N}}_0^{*}\right)\to \left(G\mathrm{RegUSGraph}K\leftrightarrow \left(G\in \mathrm{USGraph}\wedge K\in {\mathbb{N}}_0^{*}\wedge \forall v\in VD\left(v\right)=K\right)\right)$$
4	3	3adant3	$$⊢\left(G\in \mathrm{USGraph}\wedge K\in {\mathbb{N}}_0^{*}\wedge \forall v\in VD\left(v\right)=K\right)\to \left(G\mathrm{RegUSGraph}K\leftrightarrow \left(G\in \mathrm{USGraph}\wedge K\in {\mathbb{N}}_0^{*}\wedge \forall v\in VD\left(v\right)=K\right)\right)$$
5	4	ibir	$$⊢\left(G\in \mathrm{USGraph}\wedge K\in {\mathbb{N}}_0^{*}\wedge \forall v\in VD\left(v\right)=K\right)\to G\mathrm{RegUSGraph}K$$