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

Metamath Proof Explorer

Theorem isclwlk

Description: A pair of functions represents a closed walk iff it represents a walk in which the first vertex is equal to the last vertex. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 16-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion isclwlk ( 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 clwlks ⊢ ( ClWalks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) }
2 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
3 2 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
4 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
5 fveq2 ⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
6 5 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
7 4 6 fveq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
8 3 7 eqeq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
9 relwlk ⊢ Rel ( Walks ‘ 𝐺 )
10 1 8 9 brfvopabrbr ⊢ ( 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )