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 = Vtx G
usgr2wspthon0.e E = Edg G
Assertion usgr2wspthons3 G USGraph A V B V C V ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C A B E B C E

Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v V = Vtx G
2 usgr2wspthon0.e E = Edg G
3 2nn 2
4 ne0i ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A 2 WSPathsNOn G C
5 wspthsnonn0vne 2 A 2 WSPathsNOn G C A C
6 3 4 5 sylancr ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C
7 simplr G USGraph A C ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C
8 wpthswwlks2on G USGraph A C A 2 WSPathsNOn G C = A 2 WWalksNOn G C
9 8 eleq2d G USGraph A C ⟨“ ABC ”⟩ A 2 WSPathsNOn G C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
10 9 biimpa G USGraph A C ⟨“ ABC ”⟩ A 2 WSPathsNOn G C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
11 7 10 jca G USGraph A C ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
12 11 exp31 G USGraph A C ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
13 12 com13 ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C G USGraph A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
14 6 13 mpd ⟨“ ABC ”⟩ A 2 WSPathsNOn G C G USGraph A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
15 14 com12 G USGraph ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
16 9 biimprd G USGraph A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C ⟨“ ABC ”⟩ A 2 WSPathsNOn G C
17 16 expimpd G USGraph A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C ⟨“ ABC ”⟩ A 2 WSPathsNOn G C
18 15 17 impbid G USGraph ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
19 18 adantr G USGraph A V B V C V ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C
20 usgrumgr G USGraph G UMGraph
21 1 2 umgrwwlks2on G UMGraph A V B V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C A B E B C E
22 20 21 sylan G USGraph A V B V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C A B E B C E
23 22 anbi2d G USGraph A V B V C V A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C A C A B E B C E
24 3anass A C A B E B C E A C A B E B C E
25 23 24 bitr4di G USGraph A V B V C V A C ⟨“ ABC ”⟩ A 2 WWalksNOn G C A C A B E B C E
26 19 25 bitrd G USGraph A V B V C V ⟨“ ABC ”⟩ A 2 WSPathsNOn G C A C A B E B C E