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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	wwlks2onsym	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elwwlks2on.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3	1 2	umgrwwlks2on	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) )
4		3anrev	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) )
5	1 2	umgrwwlks2on	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) → ( ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ↔ ( { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ) ) )
6	4 5	sylan2b	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ↔ ( { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ) ) )
7		prcom	⊢ { 𝐶 , 𝐵 } = { 𝐵 , 𝐶 }
8	7	eleq1i	⊢ ( { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) )
9		prcom	⊢ { 𝐵 , 𝐴 } = { 𝐴 , 𝐵 }
10	9	eleq1i	⊢ ( { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
11	8 10	anbi12ci	⊢ ( ( { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) )
12	6 11	bitr2di	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) )
13	3 12	bitrd	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) )