# Metamath Proof Explorer

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
`|- E = ( Edg ` G )`
`|- I = ( iEdg ` G )`
`|- F = <" J K ">`
`|- P = <" A B C ">`
`|- ( ph -> G e. UMGraph )`
`|- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )`
`|- ( ph -> ( I ` J ) = { A , B } )`
`|- ( ph -> ( I ` K ) = { B , C } )`
`|- ( ph -> ( F ( Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) )`

### Proof

Step Hyp Ref Expression
` |-  E = ( Edg ` G )`
` |-  I = ( iEdg ` G )`
` |-  F = <" J K ">`
` |-  P = <" A B C ">`
` |-  ( ph -> G e. UMGraph )`
` |-  ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )`
` |-  ( ph -> ( I ` J ) = { A , B } )`
` |-  ( 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 ) )`
` |-  ( ( 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 ) ) ) )`