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 ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
extwwlkfab.f ⊢ F = X ClWWalksNOn ⁡ G N − 2
numclwwlk.t ⊢ T = u ∈ X C N ⟼ u prefix N − 2 u ⁡ N − 1
Assertion numclwwlk1lem2fv ⊢ W ∈ 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 ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
3 extwwlkfab.f ⊢ F = X ClWWalksNOn ⁡ G N − 2
4 numclwwlk.t ⊢ T = u ∈ 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 ∈ V
9 7 4 8 fvmpt ⊢ W ∈ X C N → T ⁡ W = W prefix N − 2 W ⁡ N − 1