Metamath Proof Explorer

Theorem revwlkb

Description: Two words represent a walk if and only if their reverses also represent a walk. (Contributed by BTernaryTau, 4-Dec-2023)

Ref Expression
Assertion revwlkb 
|- ( ( F e. Word W /\ P e. Word U ) -> ( F ( Walks ` G ) P <-> ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) ) )

Proof

Step Hyp Ref Expression
1 revwlk 
 |-  ( F ( Walks ` G ) P -> ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) )
2 revwlk 
 |-  ( ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) -> ( reverse ` ( reverse ` F ) ) ( Walks ` G ) ( reverse ` ( reverse ` P ) ) )
3 revrev 
 |-  ( F e. Word W -> ( reverse ` ( reverse ` F ) ) = F )
4 revrev 
 |-  ( P e. Word U -> ( reverse ` ( reverse ` P ) ) = P )
5 3 4 breqan12d 
 |-  ( ( F e. Word W /\ P e. Word U ) -> ( ( reverse ` ( reverse ` F ) ) ( Walks ` G ) ( reverse ` ( reverse ` P ) ) <-> F ( Walks ` G ) P ) )
6 2 5 imbitrid 
 |-  ( ( F e. Word W /\ P e. Word U ) -> ( ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) -> F ( Walks ` G ) P ) )
7 1 6 impbid2 
 |-  ( ( F e. Word W /\ P e. Word U ) -> ( F ( Walks ` G ) P <-> ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) ) )