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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	extwwlkfab.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
	extwwlkfab.f	⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
	numclwwlk.t	⊢ 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
Assertion	numclwwlk1lem2fv	⊢ ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) → ( 𝑇 ‘ 𝑊 ) = ⟨ ( 𝑊 prefix ( 𝑁 − 2 ) ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		extwwlkfab.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3		extwwlkfab.f	⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4		numclwwlk.t	⊢ 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
5		oveq1	⊢ ( 𝑢 = 𝑊 → ( 𝑢 prefix ( 𝑁 − 2 ) ) = ( 𝑊 prefix ( 𝑁 − 2 ) ) )
6		fveq1	⊢ ( 𝑢 = 𝑊 → ( 𝑢 ‘ ( 𝑁 − 1 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
7	5 6	opeq12d	⊢ ( 𝑢 = 𝑊 → ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ = ⟨ ( 𝑊 prefix ( 𝑁 − 2 ) ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) ⟩ )
8		opex	⊢ ⟨ ( 𝑊 prefix ( 𝑁 − 2 ) ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) ⟩ ∈ V
9	7 4 8	fvmpt	⊢ ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) → ( 𝑇 ‘ 𝑊 ) = ⟨ ( 𝑊 prefix ( 𝑁 − 2 ) ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) ⟩ )