# 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}=\mathrm{Edg}\left({G}\right)$
Assertion umgr2wlkon ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({A}\mathrm{WalksOn}\left({G}\right){C}\right){p}$

### Proof

Step Hyp Ref Expression
1 umgr2wlk.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
2 1 umgr2wlk ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)$
3 simp1 ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\to {f}\mathrm{Walks}\left({G}\right){p}$
4 eqcom ${⊢}{A}={p}\left(0\right)↔{p}\left(0\right)={A}$
5 4 biimpi ${⊢}{A}={p}\left(0\right)\to {p}\left(0\right)={A}$
6 5 3ad2ant1 ${⊢}\left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\to {p}\left(0\right)={A}$
7 6 3ad2ant3 ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\to {p}\left(0\right)={A}$
8 fveq2 ${⊢}2=\left|{f}\right|\to {p}\left(2\right)={p}\left(\left|{f}\right|\right)$
9 8 eqcoms ${⊢}\left|{f}\right|=2\to {p}\left(2\right)={p}\left(\left|{f}\right|\right)$
10 9 eqeq1d ${⊢}\left|{f}\right|=2\to \left({p}\left(2\right)={C}↔{p}\left(\left|{f}\right|\right)={C}\right)$
11 10 biimpcd ${⊢}{p}\left(2\right)={C}\to \left(\left|{f}\right|=2\to {p}\left(\left|{f}\right|\right)={C}\right)$
12 11 eqcoms ${⊢}{C}={p}\left(2\right)\to \left(\left|{f}\right|=2\to {p}\left(\left|{f}\right|\right)={C}\right)$
13 12 3ad2ant3 ${⊢}\left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\to \left(\left|{f}\right|=2\to {p}\left(\left|{f}\right|\right)={C}\right)$
14 13 com12 ${⊢}\left|{f}\right|=2\to \left(\left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\to {p}\left(\left|{f}\right|\right)={C}\right)$
15 14 a1i ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left(\left|{f}\right|=2\to \left(\left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\to {p}\left(\left|{f}\right|\right)={C}\right)\right)$
16 15 3imp ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\to {p}\left(\left|{f}\right|\right)={C}$
17 3 7 16 3jca ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\wedge {p}\left(0\right)={A}\wedge {p}\left(\left|{f}\right|\right)={C}\right)$
18 17 adantl ${⊢}\left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\wedge {p}\left(0\right)={A}\wedge {p}\left(\left|{f}\right|\right)={C}\right)$
19 1 umgr2adedgwlklem ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\left({A}\ne {B}\wedge {B}\ne {C}\right)\wedge \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)\right)$
20 simprr1 ${⊢}\left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left({A}\ne {B}\wedge {B}\ne {C}\right)\wedge \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)\right)\right)\to {A}\in \mathrm{Vtx}\left({G}\right)$
21 simprr3 ${⊢}\left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left({A}\ne {B}\wedge {B}\ne {C}\right)\wedge \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)\right)\right)\to {C}\in \mathrm{Vtx}\left({G}\right)$
22 20 21 jca ${⊢}\left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left({A}\ne {B}\wedge {B}\ne {C}\right)\wedge \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)\right)\right)\to \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)$
23 19 22 mpdan ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)$
24 vex ${⊢}{f}\in \mathrm{V}$
25 vex ${⊢}{p}\in \mathrm{V}$
26 24 25 pm3.2i ${⊢}\left({f}\in \mathrm{V}\wedge {p}\in \mathrm{V}\right)$
27 26 a1i ${⊢}\left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\right)\to \left({f}\in \mathrm{V}\wedge {p}\in \mathrm{V}\right)$
28 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
29 28 iswlkon ${⊢}\left(\left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({f}\in \mathrm{V}\wedge {p}\in \mathrm{V}\right)\right)\to \left({f}\left({A}\mathrm{WalksOn}\left({G}\right){C}\right){p}↔\left({f}\mathrm{Walks}\left({G}\right){p}\wedge {p}\left(0\right)={A}\wedge {p}\left(\left|{f}\right|\right)={C}\right)\right)$
30 23 27 29 syl2an2r ${⊢}\left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\right)\to \left({f}\left({A}\mathrm{WalksOn}\left({G}\right){C}\right){p}↔\left({f}\mathrm{Walks}\left({G}\right){p}\wedge {p}\left(0\right)={A}\wedge {p}\left(\left|{f}\right|\right)={C}\right)\right)$
31 18 30 mpbird ${⊢}\left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\right)\to {f}\left({A}\mathrm{WalksOn}\left({G}\right){C}\right){p}$
32 31 ex ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\to {f}\left({A}\mathrm{WalksOn}\left({G}\right){C}\right){p}\right)$
33 32 2eximdv ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({A}\mathrm{WalksOn}\left({G}\right){C}\right){p}\right)$
34 2 33 mpd ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({A}\mathrm{WalksOn}\left({G}\right){C}\right){p}$