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 )`
` |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( p ` 0 ) = A )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( 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 )`