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 𝑉 = ( 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 𝐺 ) 𝐴 ) ) )