Theorem numclwwlk1lem2fv

Description: Value of the function T . (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 31-Oct-2022)

	Ref	Expression
Hypotheses	extwwlkfab.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	extwwlkfab.c	$$⊢C=\left(v\in V,n\in {\mathbb{Z}}_{\ge 2}⟼\left\{w\in \left(v\mathrm{ClWWalksNOn}\left(G\right)n\right)|w\left(n-2\right)=v\right\}\right)$$
	extwwlkfab.f	$$⊢F=X\mathrm{ClWWalksNOn}\left(G\right)\left(N-2\right)$$
	numclwwlk.t	$$⊢T=\left(u\in \left(XCN\right)⟼⟨u\mathrm{prefix}\left(N-2\right),u\left(N-1\right)⟩\right)$$
Assertion	numclwwlk1lem2fv	$$⊢W\in \left(XCN\right)\to T\left(W\right)=⟨W\mathrm{prefix}\left(N-2\right),W\left(N-1\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		extwwlkfab.c	$$⊢C=\left(v\in V,n\in {\mathbb{Z}}_{\ge 2}⟼\left\{w\in \left(v\mathrm{ClWWalksNOn}\left(G\right)n\right)|w\left(n-2\right)=v\right\}\right)$$
3		extwwlkfab.f	$$⊢F=X\mathrm{ClWWalksNOn}\left(G\right)\left(N-2\right)$$
4		numclwwlk.t	$$⊢T=\left(u\in \left(XCN\right)⟼⟨u\mathrm{prefix}\left(N-2\right),u\left(N-1\right)⟩\right)$$
5		oveq1	$$⊢u=W\to u\mathrm{prefix}\left(N-2\right)=W\mathrm{prefix}\left(N-2\right)$$
6		fveq1	$$⊢u=W\to u\left(N-1\right)=W\left(N-1\right)$$
7	5 6	opeq12d	$$⊢u=W\to ⟨u\mathrm{prefix}\left(N-2\right),u\left(N-1\right)⟩=⟨W\mathrm{prefix}\left(N-2\right),W\left(N-1\right)⟩$$
8		opex	$$⊢⟨W\mathrm{prefix}\left(N-2\right),W\left(N-1\right)⟩\in \mathrm{V}$$
9	7 4 8	fvmpt	$$⊢W\in \left(XCN\right)\to T\left(W\right)=⟨W\mathrm{prefix}\left(N-2\right),W\left(N-1\right)⟩$$