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 
|- ( F ( ClWalks ` G ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 clwlks 
 |-  ( ClWalks ` G ) = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) }
2 fveq1 
 |-  ( p = P -> ( p ` 0 ) = ( P ` 0 ) )
3 2 adantl 
 |-  ( ( f = F /\ p = P ) -> ( p ` 0 ) = ( P ` 0 ) )
4 simpr 
 |-  ( ( f = F /\ p = P ) -> p = P )
5 fveq2 
 |-  ( f = F -> ( # ` f ) = ( # ` F ) )
6 5 adantr 
 |-  ( ( f = F /\ p = P ) -> ( # ` f ) = ( # ` F ) )
7 4 6 fveq12d 
 |-  ( ( f = F /\ p = P ) -> ( p ` ( # ` f ) ) = ( P ` ( # ` F ) ) )
8 3 7 eqeq12d 
 |-  ( ( f = F /\ p = P ) -> ( ( p ` 0 ) = ( p ` ( # ` f ) ) <-> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
9 relwlk 
 |-  Rel ( Walks ` G )
10 1 8 9 brfvopabrbr 
 |-  ( F ( ClWalks ` G ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )