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”⟩∈A2WWalksNOnGC↔⟨“CBA”⟩∈C2WWalksNOnGA

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”⟩∈A2WWalksNOnGC↔AB∈Edg⁡G∧BC∈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”⟩∈C2WWalksNOnGA↔CB∈Edg⁡G∧BA∈Edg⁡G
6 4 5 sylan2b ⊢G∈UMGraph∧A∈V∧B∈V∧C∈V→⟨“CBA”⟩∈C2WWalksNOnGA↔CB∈Edg⁡G∧BA∈Edg⁡G
7 prcom ⊢CB=BC
8 7 eleq1i ⊢CB∈Edg⁡G↔BC∈Edg⁡G
9 prcom ⊢BA=AB
10 9 eleq1i ⊢BA∈Edg⁡G↔AB∈Edg⁡G
11 8 10 anbi12ci ⊢CB∈Edg⁡G∧BA∈Edg⁡G↔AB∈Edg⁡G∧BC∈Edg⁡G
12 6 11 bitr2di ⊢G∈UMGraph∧A∈V∧B∈V∧C∈V→AB∈Edg⁡G∧BC∈Edg⁡G↔⟨“CBA”⟩∈C2WWalksNOnGA
13 3 12 bitrd ⊢G∈UMGraph∧A∈V∧B∈V∧C∈V→⟨“ABC”⟩∈A2WWalksNOnGC↔⟨“CBA”⟩∈C2WWalksNOnGA