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 ∈ Word W ∧ P ∈ 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 ∈ Word W → reverse ⁡ reverse ⁡ F = F
4 revrev ⊢ P ∈ Word U → reverse ⁡ reverse ⁡ P = P
5 3 4 breqan12d ⊢ F ∈ Word W ∧ P ∈ Word U → reverse ⁡ reverse ⁡ F Walks ⁡ G reverse ⁡ reverse ⁡ P ↔ F Walks ⁡ G P
6 2 5 imbitrid ⊢ F ∈ Word W ∧ P ∈ Word U → reverse ⁡ F Walks ⁡ G reverse ⁡ P → F Walks ⁡ G P
7 1 6 impbid2 ⊢ F ∈ Word W ∧ P ∈ Word U → F Walks ⁡ G P ↔ reverse ⁡ F Walks ⁡ G reverse ⁡ P