# 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 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgr2wlkon ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓𝑝 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑝 )

### Proof

Step Hyp Ref Expression
1 umgr2wlk.e 𝐸 = ( Edg ‘ 𝐺 )
2 1 umgr2wlk ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) )
3 simp1 ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
4 eqcom ( 𝐴 = ( 𝑝 ‘ 0 ) ↔ ( 𝑝 ‘ 0 ) = 𝐴 )
5 4 biimpi ( 𝐴 = ( 𝑝 ‘ 0 ) → ( 𝑝 ‘ 0 ) = 𝐴 )
6 5 3ad2ant1 ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝑝 ‘ 0 ) = 𝐴 )
7 6 3ad2ant3 ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑝 ‘ 0 ) = 𝐴 )
8 fveq2 ( 2 = ( ♯ ‘ 𝑓 ) → ( 𝑝 ‘ 2 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) )
9 8 eqcoms ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑝 ‘ 2 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) )
10 9 eqeq1d ( ( ♯ ‘ 𝑓 ) = 2 → ( ( 𝑝 ‘ 2 ) = 𝐶 ↔ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) )
11 10 biimpcd ( ( 𝑝 ‘ 2 ) = 𝐶 → ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) )
12 11 eqcoms ( 𝐶 = ( 𝑝 ‘ 2 ) → ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) )
13 12 3ad2ant3 ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) )
14 13 com12 ( ( ♯ ‘ 𝑓 ) = 2 → ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) )
15 14 a1i ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ♯ ‘ 𝑓 ) = 2 → ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) ) )
16 15 3imp ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 )
17 3 7 16 3jca ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) )
18 17 adantl ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) )
19 1 umgr2adedgwlklem ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
20 simprr1 ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
21 simprr3 ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
22 20 21 jca ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
23 19 22 mpdan ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
24 vex 𝑓 ∈ V
25 vex 𝑝 ∈ V
26 24 25 pm3.2i ( 𝑓 ∈ V ∧ 𝑝 ∈ V )
27 26 a1i ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( 𝑓 ∈ V ∧ 𝑝 ∈ V ) )
28 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
29 28 iswlkon ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑓 ∈ V ∧ 𝑝 ∈ V ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑝 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) ) )
30 23 27 29 syl2an2r ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑝 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐶 ) ) )
31 18 30 mpbird ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑝 )
32 31 ex ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑝 ) )
33 32 2eximdv ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ∃ 𝑓𝑝 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑝 ) )
34 2 33 mpd ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓𝑝 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑝 )