Theorem rusgrnumwwlkb1

Description: Induction base 1 for rusgrnumwwlk . (Contributed by Alexander van der Vekens, 28-Jul-2018) (Revised by AV, 7-May-2021)

	Ref	Expression
Hypotheses	rusgrnumwwlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	rusgrnumwwlk.l	$$⊢L=\left(v\in V,n\in {\mathbb{N}}_0⟼\left|\left\{w\in \left(n\mathrm{WWalksN}G\right)|w\left(0\right)=v\right\}\right|\right)$$
Assertion	rusgrnumwwlkb1	$$⊢\left(G\mathrm{RegUSGraph}K\wedge P\in V\right)\to PL1=K$$

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		rusgrnumwwlk.l	$$⊢L=\left(v\in V,n\in {\mathbb{N}}_0⟼\left|\left\{w\in \left(n\mathrm{WWalksN}G\right)|w\left(0\right)=v\right\}\right|\right)$$
3		simpr	$$⊢\left(G\mathrm{RegUSGraph}K\wedge P\in V\right)\to P\in V$$
4		1nn0	$$⊢1\in {\mathbb{N}}_0$$
5	1 2	rusgrnumwwlklem	$$⊢\left(P\in V\wedge 1\in {\mathbb{N}}_0\right)\to PL1=\left|\left\{w\in \left(1\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}\right|$$
6	3 4 5	sylancl	$$⊢\left(G\mathrm{RegUSGraph}K\wedge P\in V\right)\to PL1=\left|\left\{w\in \left(1\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}\right|$$
7	1	rusgrnumwwlkl1	$$⊢\left(G\mathrm{RegUSGraph}K\wedge P\in V\right)\to \left|\left\{w\in \left(1\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}\right|=K$$
8	6 7	eqtrd	$$⊢\left(G\mathrm{RegUSGraph}K\wedge P\in V\right)\to PL1=K$$