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	⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( reverse ‘ 𝐹 ) ( Walks ‘ 𝐺 ) ( reverse ‘ 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		revwlk	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( reverse ‘ 𝐹 ) ( Walks ‘ 𝐺 ) ( reverse ‘ 𝑃 ) )
2		revwlk	⊢ ( ( reverse ‘ 𝐹 ) ( Walks ‘ 𝐺 ) ( reverse ‘ 𝑃 ) → ( reverse ‘ ( reverse ‘ 𝐹 ) ) ( Walks ‘ 𝐺 ) ( reverse ‘ ( reverse ‘ 𝑃 ) ) )
3		revrev	⊢ ( 𝐹 ∈ Word 𝑊 → ( reverse ‘ ( reverse ‘ 𝐹 ) ) = 𝐹 )
4		revrev	⊢ ( 𝑃 ∈ Word 𝑈 → ( reverse ‘ ( reverse ‘ 𝑃 ) ) = 𝑃 )
5	3 4	breqan12d	⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈 ) → ( ( reverse ‘ ( reverse ‘ 𝐹 ) ) ( Walks ‘ 𝐺 ) ( reverse ‘ ( reverse ‘ 𝑃 ) ) ↔ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) )
6	2 5	imbitrid	⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈 ) → ( ( reverse ‘ 𝐹 ) ( Walks ‘ 𝐺 ) ( reverse ‘ 𝑃 ) → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) )
7	1 6	impbid2	⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( reverse ‘ 𝐹 ) ( Walks ‘ 𝐺 ) ( reverse ‘ 𝑃 ) ) )