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

Metamath Proof Explorer

Theorem wlkonwlk

Description: A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017) (Revised by AV, 2-Jan-2021) (Proof shortened by AV, 31-Jan-2021)

Ref Expression
Assertion wlkonwlk ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
2 eqidd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
3 eqidd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 4 wlkepvtx ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) )
6 wlkv ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
7 3simpc ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
8 6 7 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
9 4 iswlkon ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
10 5 8 9 syl2anc ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
11 1 2 3 10 mpbir3and ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 )