Metamath Proof Explorer

Theorem wwlks2onsym

Description: There is a walk of length 2 from one vertex to another vertex iff there is a walk of length 2 from the other vertex to the first vertex. (Contributed by AV, 7-Jan-2022)

Ref Expression
Hypothesis elwwlks2on.v ⊢ V = Vtx ⁡ G
Assertion wwlks2onsym ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ⟨“ CBA ”⟩ ∈ C 2 WWalksNOn G A

Proof

Step Hyp Ref Expression
1 elwwlks2on.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 umgrwwlks2on ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ A B ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G
4 3anrev ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ C ∈ V ∧ B ∈ V ∧ A ∈ V
5 1 2 umgrwwlks2on ⊢ G ∈ UMGraph ∧ C ∈ V ∧ B ∈ V ∧ A ∈ V → ⟨“ CBA ”⟩ ∈ C 2 WWalksNOn G A ↔ C B ∈ Edg ⁡ G ∧ B A ∈ Edg ⁡ G
6 4 5 sylan2b ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ CBA ”⟩ ∈ C 2 WWalksNOn G A ↔ C B ∈ Edg ⁡ G ∧ B A ∈ Edg ⁡ G
7 prcom ⊢ C B = B C
8 7 eleq1i ⊢ C B ∈ Edg ⁡ G ↔ B C ∈ Edg ⁡ G
9 prcom ⊢ B A = A B
10 9 eleq1i ⊢ B A ∈ Edg ⁡ G ↔ A B ∈ Edg ⁡ G
11 8 10 anbi12ci ⊢ C B ∈ Edg ⁡ G ∧ B A ∈ Edg ⁡ G ↔ A B ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G
12 6 11 bitr2di ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A B ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G ↔ ⟨“ CBA ”⟩ ∈ C 2 WWalksNOn G A
13 3 12 bitrd ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ⟨“ CBA ”⟩ ∈ C 2 WWalksNOn G A