# Metamath Proof Explorer

## Theorem usgr2wspthons3

Description: A simple path of length 2 between two vertices represented as length 3 string corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypotheses usgr2wspthon0.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
usgr2wspthon0.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion usgr2wspthons3 ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\left({A}\ne {C}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$

### Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 usgr2wspthon0.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 2nn ${⊢}2\in ℕ$
4 ne0i ${⊢}⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\to {A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\ne \varnothing$
5 wspthsnonn0vne ${⊢}\left(2\in ℕ\wedge {A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\ne \varnothing \right)\to {A}\ne {C}$
6 3 4 5 sylancr ${⊢}⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\to {A}\ne {C}$
7 simplr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {A}\ne {C}\right)\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)\to {A}\ne {C}$
8 wpthswwlks2on ${⊢}\left({G}\in \mathrm{USGraph}\wedge {A}\ne {C}\right)\to {A}\left(2\mathrm{WSPathsNOn}{G}\right){C}={A}\left(2\mathrm{WWalksNOn}{G}\right){C}$
9 8 eleq2d ${⊢}\left({G}\in \mathrm{USGraph}\wedge {A}\ne {C}\right)\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)$
10 9 biimpa ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {A}\ne {C}\right)\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)\to ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)$
11 7 10 jca ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {A}\ne {C}\right)\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)\to \left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)$
12 11 exp31 ${⊢}{G}\in \mathrm{USGraph}\to \left({A}\ne {C}\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\to \left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)\right)\right)$
13 12 com13 ${⊢}⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\to \left({A}\ne {C}\to \left({G}\in \mathrm{USGraph}\to \left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)\right)\right)$
14 6 13 mpd ${⊢}⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\to \left({G}\in \mathrm{USGraph}\to \left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)\right)$
15 14 com12 ${⊢}{G}\in \mathrm{USGraph}\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\to \left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)\right)$
16 9 biimprd ${⊢}\left({G}\in \mathrm{USGraph}\wedge {A}\ne {C}\right)\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\to ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)$
17 16 expimpd ${⊢}{G}\in \mathrm{USGraph}\to \left(\left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)\to ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)$
18 15 17 impbid ${⊢}{G}\in \mathrm{USGraph}\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)\right)$
19 18 adantr ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)\right)$
20 usgrumgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\in \mathrm{UMGraph}$
21 1 2 umgrwwlks2on ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)↔\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
22 20 21 sylan ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)↔\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
23 22 anbi2d ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to \left(\left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)↔\left({A}\ne {C}\wedge \left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)\right)$
24 3anass ${⊢}\left({A}\ne {C}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)↔\left({A}\ne {C}\wedge \left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
25 23 24 syl6bbr ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to \left(\left({A}\ne {C}\wedge ⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WWalksNOn}{G}\right){C}\right)\right)↔\left({A}\ne {C}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
26 19 25 bitrd ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to \left(⟨“{A}{B}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\left({A}\ne {C}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$