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

Metamath Proof Explorer

Theorem iswlkon

Description: Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017) (Revised by AV, 31-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypothesis wlkson.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion iswlkon ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 wlkson.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 wlkson ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) } )
3 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
4 3 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
5 4 eqeq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑝 ‘ 0 ) = 𝐴 ↔ ( 𝑃 ‘ 0 ) = 𝐴 ) )
6 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
7 fveq2 ⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
8 7 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
9 6 8 fveq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
10 9 eqeq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) )
11 2 5 10 2rbropap ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
12 11 3expb ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )