Metamath Proof Explorer

Theorem umgr2wlkon

Description: For each pair of adjacent edges in a multigraph, there is a walk of length 2 between the not common vertices of the 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 umgr2wlkon 
|- ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. f E. p f ( A ( WalksOn ` G ) C ) p )

Proof

Step Hyp Ref Expression
1 umgr2wlk.e 
 |-  E = ( Edg ` G )
2 1 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 ) ) ) )
3 simp1 
 |-  ( ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> f ( Walks ` G ) p )
4 eqcom 
 |-  ( A = ( p ` 0 ) <-> ( p ` 0 ) = A )
5 4 biimpi 
 |-  ( A = ( p ` 0 ) -> ( p ` 0 ) = A )
6 5 3ad2ant1 
 |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( p ` 0 ) = A )
7 6 3ad2ant3 
 |-  ( ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( p ` 0 ) = A )
8 fveq2 
 |-  ( 2 = ( # ` f ) -> ( p ` 2 ) = ( p ` ( # ` f ) ) )
9 8 eqcoms 
 |-  ( ( # ` f ) = 2 -> ( p ` 2 ) = ( p ` ( # ` f ) ) )
10 9 eqeq1d 
 |-  ( ( # ` f ) = 2 -> ( ( p ` 2 ) = C <-> ( p ` ( # ` f ) ) = C ) )
11 10 biimpcd 
 |-  ( ( p ` 2 ) = C -> ( ( # ` f ) = 2 -> ( p ` ( # ` f ) ) = C ) )
12 11 eqcoms 
 |-  ( C = ( p ` 2 ) -> ( ( # ` f ) = 2 -> ( p ` ( # ` f ) ) = C ) )
13 12 3ad2ant3 
 |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( ( # ` f ) = 2 -> ( p ` ( # ` f ) ) = C ) )
14 13 com12 
 |-  ( ( # ` f ) = 2 -> ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( p ` ( # ` f ) ) = C ) )
15 14 a1i 
 |-  ( f ( Walks ` G ) p -> ( ( # ` f ) = 2 -> ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( p ` ( # ` f ) ) = C ) ) )
16 15 3imp 
 |-  ( ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( p ` ( # ` f ) ) = C )
17 3 7 16 3jca 
 |-  ( ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = C ) )
18 17 adantl 
 |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = C ) )
19 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 ) ) ) )
20 simprr1 
 |-  ( ( ( 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 ) ) ) ) -> A e. ( Vtx ` G ) )
21 simprr3 
 |-  ( ( ( 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 ) ) ) ) -> C e. ( Vtx ` G ) )
22 20 21 jca 
 |-  ( ( ( 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 ) ) ) ) -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
23 19 22 mpdan 
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
24 vex 
 |-  f e. _V
25 vex 
 |-  p e. _V
26 24 25 pm3.2i 
 |-  ( f e. _V /\ p e. _V )
27 26 a1i 
 |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( f e. _V /\ p e. _V ) )
28 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
29 28 iswlkon 
 |-  ( ( ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) /\ ( f e. _V /\ p e. _V ) ) -> ( f ( A ( WalksOn ` G ) C ) p <-> ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = C ) ) )
30 23 27 29 syl2an2r 
 |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( f ( A ( WalksOn ` G ) C ) p <-> ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = C ) ) )
31 18 30 mpbird 
 |-  ( ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) /\ ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> f ( A ( WalksOn ` G ) C ) p )
32 31 ex 
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> f ( A ( WalksOn ` G ) C ) p ) )
33 32 2eximdv 
 |-  ( ( 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 ) ) ) -> E. f E. p f ( A ( WalksOn ` G ) C ) p ) )
34 2 33 mpd 
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. f E. p f ( A ( WalksOn ` G ) C ) p )