This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Closed walks as words Closed walks of a fixed length as words clwwlkfv
Description: Lemma 2 for clwwlkf1o : the value of function F . (Contributed by Alexander van der Vekens , 28-Sep-2018) (Revised by AV , 26-Apr-2021)
(Revised by AV , 1-Nov-2022)
Ref
Expression
Hypotheses
clwwlkf1o.d ⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
clwwlkf1o.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
Assertion
clwwlkfv ⊢ ( 𝑊 ∈ 𝐷 → ( 𝐹 ‘ 𝑊 ) = ( 𝑊 prefix 𝑁 ) )
Proof
Step
Hyp
Ref
Expression
1
clwwlkf1o.d ⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
2
clwwlkf1o.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
3
oveq1 ⊢ ( 𝑡 = 𝑊 → ( 𝑡 prefix 𝑁 ) = ( 𝑊 prefix 𝑁 ) )
4
ovex ⊢ ( 𝑊 prefix 𝑁 ) ∈ V
5
3 2 4
fvmpt ⊢ ( 𝑊 ∈ 𝐷 → ( 𝐹 ‘ 𝑊 ) = ( 𝑊 prefix 𝑁 ) )