Metamath Proof Explorer

Theorem umgr2adedgwlk

Description: In a multigraph, two adjacent edges form a walk of length 2. (Contributed by Alexander van der Vekens, 18-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 } )
Assertion umgr2adedgwlk 
|- ( ph -> ( F ( Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) )

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 3anass 
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) <-> ( G e. UMGraph /\ ( { A , B } e. E /\ { B , C } e. E ) ) )
10 5 6 9 sylanbrc 
 |-  ( ph -> ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) )
11 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 ) ) ) )
12 10 11 syl 
 |-  ( ph -> ( ( A =/= B /\ B =/= C ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )
13 12 simprd 
 |-  ( ph -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
14 12 simpld 
 |-  ( ph -> ( A =/= B /\ B =/= C ) )
15 ssid 
 |-  { A , B } C_ { A , B }
16 15 7 sseqtrrid 
 |-  ( ph -> { A , B } C_ ( I ` J ) )
17 ssid 
 |-  { B , C } C_ { B , C }
18 17 8 sseqtrrid 
 |-  ( ph -> { B , C } C_ ( I ` K ) )
19 16 18 jca 
 |-  ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )
20 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
21 4 3 13 14 19 20 2 2wlkd 
 |-  ( ph -> F ( Walks ` G ) P )
22 3 fveq2i 
 |-  ( # ` F ) = ( # ` <" J K "> )
23 s2len 
 |-  ( # ` <" J K "> ) = 2
24 22 23 eqtri 
 |-  ( # ` F ) = 2
25 24 a1i 
 |-  ( ph -> ( # ` F ) = 2 )
26 s3fv0 
 |-  ( A e. ( Vtx ` G ) -> ( <" A B C "> ` 0 ) = A )
27 s3fv1 
 |-  ( B e. ( Vtx ` G ) -> ( <" A B C "> ` 1 ) = B )
28 s3fv2 
 |-  ( C e. ( Vtx ` G ) -> ( <" A B C "> ` 2 ) = C )
29 26 27 28 3anim123i 
 |-  ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) -> ( ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 1 ) = B /\ ( <" A B C "> ` 2 ) = C ) )
30 13 29 syl 
 |-  ( ph -> ( ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 1 ) = B /\ ( <" A B C "> ` 2 ) = C ) )
31 4 fveq1i 
 |-  ( P ` 0 ) = ( <" A B C "> ` 0 )
32 31 eqeq2i 
 |-  ( A = ( P ` 0 ) <-> A = ( <" A B C "> ` 0 ) )
33 eqcom 
 |-  ( A = ( <" A B C "> ` 0 ) <-> ( <" A B C "> ` 0 ) = A )
34 32 33 bitri 
 |-  ( A = ( P ` 0 ) <-> ( <" A B C "> ` 0 ) = A )
35 4 fveq1i 
 |-  ( P ` 1 ) = ( <" A B C "> ` 1 )
36 35 eqeq2i 
 |-  ( B = ( P ` 1 ) <-> B = ( <" A B C "> ` 1 ) )
37 eqcom 
 |-  ( B = ( <" A B C "> ` 1 ) <-> ( <" A B C "> ` 1 ) = B )
38 36 37 bitri 
 |-  ( B = ( P ` 1 ) <-> ( <" A B C "> ` 1 ) = B )
39 4 fveq1i 
 |-  ( P ` 2 ) = ( <" A B C "> ` 2 )
40 39 eqeq2i 
 |-  ( C = ( P ` 2 ) <-> C = ( <" A B C "> ` 2 ) )
41 eqcom 
 |-  ( C = ( <" A B C "> ` 2 ) <-> ( <" A B C "> ` 2 ) = C )
42 40 41 bitri 
 |-  ( C = ( P ` 2 ) <-> ( <" A B C "> ` 2 ) = C )
43 34 38 42 3anbi123i 
 |-  ( ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) <-> ( ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 1 ) = B /\ ( <" A B C "> ` 2 ) = C ) )
44 30 43 sylibr 
 |-  ( ph -> ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) )
45 21 25 44 3jca 
 |-  ( ph -> ( F ( Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) )