This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkprop

Description: Properties of a walk. (Contributed by AV, 5-Nov-2021)

Ref Expression
Hypotheses wksfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion wlkprop ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wksfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 1 2 wksfval ⊢ ( 𝐺 ∈ V → ( Walks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } )
4 3 brfvopab ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
5 1 2 iswlk ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
6 5 biimpd ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
7 4 6 mpcom ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )