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 \in Word W \land P \in Word U) \to (F Walks (G) P \leftrightarrow reverse (F) Walks (G) reverse (P))$

Step	Hyp	Ref	Expression
1		revwlk	$⊢ F Walks (G) P \to reverse (F) Walks (G) reverse (P)$
2		revwlk	$⊢ reverse (F) Walks (G) reverse (P) \to reverse (reverse (F)) Walks (G) reverse (reverse (P))$
3		revrev	$⊢ F \in Word W \to reverse (reverse (F)) = F$
4		revrev	$⊢ P \in Word U \to reverse (reverse (P)) = P$
5	3 4	breqan12d	$⊢ (F \in Word W \land P \in Word U) \to (reverse (reverse (F)) Walks (G) reverse (reverse (P)) \leftrightarrow F Walks (G) P)$
6	2 5	syl5ib	$⊢ (F \in Word W \land P \in Word U) \to (reverse (F) Walks (G) reverse (P) \to F Walks (G) P)$
7	1 6	impbid2	$⊢ (F \in Word W \land P \in Word U) \to (F Walks (G) P \leftrightarrow reverse (F) Walks (G) reverse (P))$

Metamath Proof Explorer