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 e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) <-> ( A =/= C /\ { A , B } e. E /\ { B , C } e. E ) ) )

Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v 
 |-  V = ( Vtx ` G )
2 usgr2wspthon0.e 
 |-  E = ( Edg ` G )
3 2nn 
 |-  2 e. NN
4 ne0i 
 |-  ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) -> ( A ( 2 WSPathsNOn G ) C ) =/= (/) )
5 wspthsnonn0vne 
 |-  ( ( 2 e. NN /\ ( A ( 2 WSPathsNOn G ) C ) =/= (/) ) -> A =/= C )
6 3 4 5 sylancr 
 |-  ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) -> A =/= C )
7 simplr 
 |-  ( ( ( G e. USGraph /\ A =/= C ) /\ <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> A =/= C )
8 wpthswwlks2on 
 |-  ( ( G e. USGraph /\ A =/= C ) -> ( A ( 2 WSPathsNOn G ) C ) = ( A ( 2 WWalksNOn G ) C ) )
9 8 eleq2d 
 |-  ( ( G e. USGraph /\ A =/= C ) -> ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) <-> <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
10 9 biimpa 
 |-  ( ( ( G e. USGraph /\ A =/= C ) /\ <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) )
11 7 10 jca 
 |-  ( ( ( G e. USGraph /\ A =/= C ) /\ <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
12 11 exp31 
 |-  ( G e. USGraph -> ( A =/= C -> ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) -> ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) ) )
13 12 com13 
 |-  ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) -> ( A =/= C -> ( G e. USGraph -> ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) ) )
14 6 13 mpd 
 |-  ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) -> ( G e. USGraph -> ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) )
15 14 com12 
 |-  ( G e. USGraph -> ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) -> ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) )
16 9 biimprd 
 |-  ( ( G e. USGraph /\ A =/= C ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) -> <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) ) )
17 16 expimpd 
 |-  ( G e. USGraph -> ( ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) ) )
18 15 17 impbid 
 |-  ( G e. USGraph -> ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) <-> ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) )
19 18 adantr 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) <-> ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) )
20 usgrumgr 
 |-  ( G e. USGraph -> G e. UMGraph )
21 1 2 umgrwwlks2on 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( { A , B } e. E /\ { B , C } e. E ) ) )
22 20 21 sylan 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( { A , B } e. E /\ { B , C } e. E ) ) )
23 22 anbi2d 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> ( A =/= C /\ ( { A , B } e. E /\ { B , C } e. E ) ) ) )
24 3anass 
 |-  ( ( A =/= C /\ { A , B } e. E /\ { B , C } e. E ) <-> ( A =/= C /\ ( { A , B } e. E /\ { B , C } e. E ) ) )
25 23 24 bitr4di 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A =/= C /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> ( A =/= C /\ { A , B } e. E /\ { B , C } e. E ) ) )
26 19 25 bitrd 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WSPathsNOn G ) C ) <-> ( A =/= C /\ { A , B } e. E /\ { B , C } e. E ) ) )