Metamath Proof Explorer

Theorem umgr2adedgspth

Description: In a multigraph, two adjacent edges with different endvertices form a simple path of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018) (Revised by AV, 29-Jan-2021)

Ref Expression
Hypotheses umgr2adedgwlk.e 
|- E = ( Edg ` G )
umgr2adedgwlk.i 
|- I = ( iEdg ` G )
umgr2adedgwlk.f 
|- F = <" J K ">
umgr2adedgwlk.p 
|- P = <" A B C ">
umgr2adedgwlk.g 
|- ( ph -> G e. UMGraph )
umgr2adedgwlk.a 
|- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )
umgr2adedgwlk.j 
|- ( ph -> ( I ` J ) = { A , B } )
umgr2adedgwlk.k 
|- ( ph -> ( I ` K ) = { B , C } )
umgr2adedgspth.n 
|- ( ph -> A =/= C )
Assertion umgr2adedgspth 
|- ( ph -> F ( SPaths ` G ) P )

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e 
 |-  E = ( Edg ` G )
2 umgr2adedgwlk.i 
 |-  I = ( iEdg ` G )
3 umgr2adedgwlk.f 
 |-  F = <" J K ">
4 umgr2adedgwlk.p 
 |-  P = <" A B C ">
5 umgr2adedgwlk.g 
 |-  ( ph -> G e. UMGraph )
6 umgr2adedgwlk.a 
 |-  ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )
7 umgr2adedgwlk.j 
 |-  ( ph -> ( I ` J ) = { A , B } )
8 umgr2adedgwlk.k 
 |-  ( ph -> ( I ` K ) = { B , C } )
9 umgr2adedgspth.n 
 |-  ( ph -> A =/= C )
10 3anass 
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) <-> ( G e. UMGraph /\ ( { A , B } e. E /\ { B , C } e. E ) ) )
11 5 6 10 sylanbrc 
 |-  ( ph -> ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) )
12 1 umgr2adedgwlklem 
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( ( A =/= B /\ B =/= C ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )
13 11 12 syl 
 |-  ( ph -> ( ( A =/= B /\ B =/= C ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )
14 13 simprd 
 |-  ( ph -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
15 13 simpld 
 |-  ( ph -> ( A =/= B /\ B =/= C ) )
16 ssid 
 |-  { A , B } C_ { A , B }
17 16 7 sseqtrrid 
 |-  ( ph -> { A , B } C_ ( I ` J ) )
18 ssid 
 |-  { B , C } C_ { B , C }
19 18 8 sseqtrrid 
 |-  ( ph -> { B , C } C_ ( I ` K ) )
20 17 19 jca 
 |-  ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )
21 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
22 fveq2 
 |-  ( K = J -> ( I ` K ) = ( I ` J ) )
23 22 eqcoms 
 |-  ( J = K -> ( I ` K ) = ( I ` J ) )
24 23 eqeq1d 
 |-  ( J = K -> ( ( I ` K ) = { B , C } <-> ( I ` J ) = { B , C } ) )
25 eqtr2 
 |-  ( ( ( I ` J ) = { B , C } /\ ( I ` J ) = { A , B } ) -> { B , C } = { A , B } )
26 25 ex 
 |-  ( ( I ` J ) = { B , C } -> ( ( I ` J ) = { A , B } -> { B , C } = { A , B } ) )
27 24 26 syl6bi 
 |-  ( J = K -> ( ( I ` K ) = { B , C } -> ( ( I ` J ) = { A , B } -> { B , C } = { A , B } ) ) )
28 27 com13 
 |-  ( ( I ` J ) = { A , B } -> ( ( I ` K ) = { B , C } -> ( J = K -> { B , C } = { A , B } ) ) )
29 7 8 28 sylc 
 |-  ( ph -> ( J = K -> { B , C } = { A , B } ) )
30 eqcom 
 |-  ( { B , C } = { A , B } <-> { A , B } = { B , C } )
31 prcom 
 |-  { B , C } = { C , B }
32 31 eqeq2i 
 |-  ( { A , B } = { B , C } <-> { A , B } = { C , B } )
33 30 32 bitri 
 |-  ( { B , C } = { A , B } <-> { A , B } = { C , B } )
34 21 1 umgrpredgv 
 |-  ( ( G e. UMGraph /\ { A , B } e. E ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
35 34 simpld 
 |-  ( ( G e. UMGraph /\ { A , B } e. E ) -> A e. ( Vtx ` G ) )
36 35 ex 
 |-  ( G e. UMGraph -> ( { A , B } e. E -> A e. ( Vtx ` G ) ) )
37 21 1 umgrpredgv 
 |-  ( ( G e. UMGraph /\ { B , C } e. E ) -> ( B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
38 37 simprd 
 |-  ( ( G e. UMGraph /\ { B , C } e. E ) -> C e. ( Vtx ` G ) )
39 38 ex 
 |-  ( G e. UMGraph -> ( { B , C } e. E -> C e. ( Vtx ` G ) ) )
40 36 39 anim12d 
 |-  ( G e. UMGraph -> ( ( { A , B } e. E /\ { B , C } e. E ) -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )
41 5 6 40 sylc 
 |-  ( ph -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
42 preqr1g 
 |-  ( ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) -> ( { A , B } = { C , B } -> A = C ) )
43 41 42 syl 
 |-  ( ph -> ( { A , B } = { C , B } -> A = C ) )
44 eqneqall 
 |-  ( A = C -> ( A =/= C -> J =/= K ) )
45 43 9 44 syl6ci 
 |-  ( ph -> ( { A , B } = { C , B } -> J =/= K ) )
46 33 45 syl5bi 
 |-  ( ph -> ( { B , C } = { A , B } -> J =/= K ) )
47 29 46 syld 
 |-  ( ph -> ( J = K -> J =/= K ) )
48 neqne 
 |-  ( -. J = K -> J =/= K )
49 47 48 pm2.61d1 
 |-  ( ph -> J =/= K )
50 4 3 14 15 20 21 2 49 9 2spthd 
 |-  ( ph -> F ( SPaths ` G ) P )