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 bitrid 
 |-  ( 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 bitrid 
 |-  ( 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 ) )
25 24 adantr 
 |-  ( ( ( 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 } )
28 27 adantl 
 |-  ( ( ( 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 } )
31 30 adantl 
 |-  ( ( ( 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 ) )
35 34 adantr 
 |-  ( ( 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 ) ) ) )
43 42 adantl 
 |-  ( ( 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 ) ) ) )