Metamath Proof Explorer

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 = ( Vtx ` G )
extwwlkfab.c 
|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
extwwlkfab.f 
|- F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
numclwwlk.t 
|- T = ( u e. ( X C N ) |-> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
Assertion numclwwlk1lem2fv 
|- ( W e. ( X C N ) -> ( T ` W ) = <. ( W prefix ( N - 2 ) ) , ( W ` ( N - 1 ) ) >. )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v 
 |-  V = ( Vtx ` G )
2 extwwlkfab.c 
 |-  C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
3 extwwlkfab.f 
 |-  F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
4 numclwwlk.t 
 |-  T = ( u e. ( X C N ) |-> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
5 oveq1 
 |-  ( u = W -> ( u prefix ( N - 2 ) ) = ( W prefix ( N - 2 ) ) )
6 fveq1 
 |-  ( u = W -> ( u ` ( N - 1 ) ) = ( W ` ( N - 1 ) ) )
7 5 6 opeq12d 
 |-  ( u = W -> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. = <. ( W prefix ( N - 2 ) ) , ( W ` ( N - 1 ) ) >. )
8 opex 
 |-  <. ( W prefix ( N - 2 ) ) , ( W ` ( N - 1 ) ) >. e. _V
9 7 4 8 fvmpt 
 |-  ( W e. ( X C N ) -> ( T ` W ) = <. ( W prefix ( N - 2 ) ) , ( W ` ( N - 1 ) ) >. )