# Metamath Proof Explorer

## Theorem umgr2wlk

Description: In a multigraph, there is a walk of length 2 for each pair of adjacent edges. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 30-Jan-2021)

Ref Expression
Hypothesis umgr2wlk.e
`|- E = ( Edg ` G )`
Assertion umgr2wlk
`|- ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) )`

### Proof

Step Hyp Ref Expression
1 umgr2wlk.e
` |-  E = ( Edg ` G )`
2 umgruhgr
` |-  ( G e. UMGraph -> G e. UHGraph )`
3 1 eleq2i
` |-  ( { B , C } e. E <-> { B , C } e. ( Edg ` G ) )`
4 eqid
` |-  ( iEdg ` G ) = ( iEdg ` G )`
5 4 uhgredgiedgb
` |-  ( G e. UHGraph -> ( { B , C } e. ( Edg ` G ) <-> E. i e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` i ) ) )`
6 3 5 syl5bb
` |-  ( G e. UHGraph -> ( { B , C } e. E <-> E. i e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` i ) ) )`
7 2 6 syl
` |-  ( G e. UMGraph -> ( { B , C } e. E <-> E. i e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` i ) ) )`
8 7 biimpd
` |-  ( G e. UMGraph -> ( { B , C } e. E -> E. i e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` i ) ) )`
9 8 a1d
` |-  ( G e. UMGraph -> ( { A , B } e. E -> ( { B , C } e. E -> E. i e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` i ) ) ) )`
10 9 3imp
` |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. i e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` i ) )`
11 1 eleq2i
` |-  ( { A , B } e. E <-> { A , B } e. ( Edg ` G ) )`
12 4 uhgredgiedgb
` |-  ( G e. UHGraph -> ( { A , B } e. ( Edg ` G ) <-> E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) ) )`
13 11 12 syl5bb
` |-  ( G e. UHGraph -> ( { A , B } e. E <-> E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) ) )`
14 2 13 syl
` |-  ( G e. UMGraph -> ( { A , B } e. E <-> E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) ) )`
15 14 biimpd
` |-  ( G e. UMGraph -> ( { A , B } e. E -> E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) ) )`
16 15 a1dd
` |-  ( G e. UMGraph -> ( { A , B } e. E -> ( { B , C } e. E -> E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) ) ) )`
17 16 3imp
` |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) )`
18 s2cli
` |-  <" j i "> e. Word _V`
19 s3cli
` |-  <" A B C "> e. Word _V`
20 18 19 pm3.2i
` |-  ( <" j i "> e. Word _V /\ <" A B C "> e. Word _V )`
21 eqid
` |-  <" j i "> = <" j i ">`
22 eqid
` |-  <" A B C "> = <" A B C ">`
23 simpl1
` |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) ) -> G e. UMGraph )`
24 3simpc
` |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( { A , B } e. E /\ { B , C } e. E ) )`
` |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) ) -> ( { A , B } e. E /\ { B , C } e. E ) )`
26 simpl
` |-  ( ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) -> { A , B } = ( ( iEdg ` G ) ` j ) )`
27 26 eqcomd
` |-  ( ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` G ) ` j ) = { A , B } )`
` |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) ) -> ( ( iEdg ` G ) ` j ) = { A , B } )`
29 simpr
` |-  ( ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) -> { B , C } = ( ( iEdg ` G ) ` i ) )`
30 29 eqcomd
` |-  ( ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` G ) ` i ) = { B , C } )`
` |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) ) -> ( ( iEdg ` G ) ` i ) = { B , C } )`
32 1 4 21 22 23 25 28 31 umgr2adedgwlk
` |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) ) -> ( <" j i "> ( Walks ` G ) <" A B C "> /\ ( # ` <" j i "> ) = 2 /\ ( A = ( <" A B C "> ` 0 ) /\ B = ( <" A B C "> ` 1 ) /\ C = ( <" A B C "> ` 2 ) ) ) )`
33 breq12
` |-  ( ( f = <" j i "> /\ p = <" A B C "> ) -> ( f ( Walks ` G ) p <-> <" j i "> ( Walks ` G ) <" A B C "> ) )`
34 fveqeq2
` |-  ( f = <" j i "> -> ( ( # ` f ) = 2 <-> ( # ` <" j i "> ) = 2 ) )`
` |-  ( ( f = <" j i "> /\ p = <" A B C "> ) -> ( ( # ` f ) = 2 <-> ( # ` <" j i "> ) = 2 ) )`
36 fveq1
` |-  ( p = <" A B C "> -> ( p ` 0 ) = ( <" A B C "> ` 0 ) )`
37 36 eqeq2d
` |-  ( p = <" A B C "> -> ( A = ( p ` 0 ) <-> A = ( <" A B C "> ` 0 ) ) )`
38 fveq1
` |-  ( p = <" A B C "> -> ( p ` 1 ) = ( <" A B C "> ` 1 ) )`
39 38 eqeq2d
` |-  ( p = <" A B C "> -> ( B = ( p ` 1 ) <-> B = ( <" A B C "> ` 1 ) ) )`
40 fveq1
` |-  ( p = <" A B C "> -> ( p ` 2 ) = ( <" A B C "> ` 2 ) )`
41 40 eqeq2d
` |-  ( p = <" A B C "> -> ( C = ( p ` 2 ) <-> C = ( <" A B C "> ` 2 ) ) )`
42 37 39 41 3anbi123d
` |-  ( p = <" A B C "> -> ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) <-> ( A = ( <" A B C "> ` 0 ) /\ B = ( <" A B C "> ` 1 ) /\ C = ( <" A B C "> ` 2 ) ) ) )`
` |-  ( ( f = <" j i "> /\ p = <" A B C "> ) -> ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) <-> ( A = ( <" A B C "> ` 0 ) /\ B = ( <" A B C "> ` 1 ) /\ C = ( <" A B C "> ` 2 ) ) ) )`
44 33 35 43 3anbi123d
` |-  ( ( f = <" j i "> /\ p = <" A B C "> ) -> ( ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) <-> ( <" j i "> ( Walks ` G ) <" A B C "> /\ ( # ` <" j i "> ) = 2 /\ ( A = ( <" A B C "> ` 0 ) /\ B = ( <" A B C "> ` 1 ) /\ C = ( <" A B C "> ` 2 ) ) ) ) )`
45 44 spc2egv
` |-  ( ( <" j i "> e. Word _V /\ <" A B C "> e. Word _V ) -> ( ( <" j i "> ( Walks ` G ) <" A B C "> /\ ( # ` <" j i "> ) = 2 /\ ( A = ( <" A B C "> ` 0 ) /\ B = ( <" A B C "> ` 1 ) /\ C = ( <" A B C "> ` 2 ) ) ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) )`
46 20 32 45 mpsyl
` |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( { A , B } = ( ( iEdg ` G ) ` j ) /\ { B , C } = ( ( iEdg ` G ) ` i ) ) ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) )`
47 46 exp32
` |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( { A , B } = ( ( iEdg ` G ) ` j ) -> ( { B , C } = ( ( iEdg ` G ) ` i ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )`
48 47 com12
` |-  ( { A , B } = ( ( iEdg ` G ) ` j ) -> ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( { B , C } = ( ( iEdg ` G ) ` i ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )`
49 48 rexlimivw
` |-  ( E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) -> ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( { B , C } = ( ( iEdg ` G ) ` i ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )`
50 49 com13
` |-  ( { B , C } = ( ( iEdg ` G ) ` i ) -> ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )`
51 50 rexlimivw
` |-  ( E. i e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` i ) -> ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )`
52 51 com12
` |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( E. i e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` i ) -> ( E. j e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` j ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )`
53 10 17 52 mp2d
` |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) )`