Theorem rusgrnumwwlklem

Description: Lemma for rusgrnumwwlk etc. (Contributed by Alexander van der Vekens, 21-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	rusgrnumwwlklem	$$⊢\left(P\in V\wedge N\in {\mathbb{N}}_0\right)\to PLN=\left|\left\{w\in \left(N\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}\right|$$

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		oveq1	$$⊢n=N\to n\mathrm{WWalksN}G=N\mathrm{WWalksN}G$$
4	3	adantl	$$⊢\left(v=P\wedge n=N\right)\to n\mathrm{WWalksN}G=N\mathrm{WWalksN}G$$
5		eqeq2	$$⊢v=P\to \left(w\left(0\right)=v\leftrightarrow w\left(0\right)=P\right)$$
6	5	adantr	$$⊢\left(v=P\wedge n=N\right)\to \left(w\left(0\right)=v\leftrightarrow w\left(0\right)=P\right)$$
7	4 6	rabeqbidv	$$⊢\left(v=P\wedge n=N\right)\to \left\{w\in \left(n\mathrm{WWalksN}G\right)|w\left(0\right)=v\right\}=\left\{w\in \left(N\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}$$
8	7	fveq2d	$$⊢\left(v=P\wedge n=N\right)\to \left|\left\{w\in \left(n\mathrm{WWalksN}G\right)|w\left(0\right)=v\right\}\right|=\left|\left\{w\in \left(N\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}\right|$$
9		fvex	$$⊢\left|\left\{w\in \left(N\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}\right|\in \mathrm{V}$$
10	8 2 9	ovmpoa	$$⊢\left(P\in V\wedge N\in {\mathbb{N}}_0\right)\to PLN=\left|\left\{w\in \left(N\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}\right|$$