Theorem rgrprop

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

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

Proof

Step	Hyp	Ref	Expression
1		isrgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isrgr.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
3		df-rgr	$$⊢\mathrm{RegGraph}=\left\{⟨g,k⟩|\left(k\in {\mathbb{N}}_0^{*}\wedge \forall v\in \mathrm{Vtx}\left(g\right)\mathrm{VtxDeg}\left(g\right)\left(v\right)=k\right)\right\}$$
4	3	bropaex12	$$⊢G\mathrm{RegGraph}K\to \left(G\in \mathrm{V}\wedge K\in \mathrm{V}\right)$$
5	1 2	isrgr	$$⊢\left(G\in \mathrm{V}\wedge K\in \mathrm{V}\right)\to \left(G\mathrm{RegGraph}K\leftrightarrow \left(K\in {\mathbb{N}}_0^{*}\wedge \forall v\in VD\left(v\right)=K\right)\right)$$
6	5	biimpd	$$⊢\left(G\in \mathrm{V}\wedge K\in \mathrm{V}\right)\to \left(G\mathrm{RegGraph}K\to \left(K\in {\mathbb{N}}_0^{*}\wedge \forall v\in VD\left(v\right)=K\right)\right)$$
7	4 6	mpcom	$$⊢G\mathrm{RegGraph}K\to \left(K\in {\mathbb{N}}_0^{*}\wedge \forall v\in VD\left(v\right)=K\right)$$