# 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}=\mathrm{Edg}\left({G}\right)$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 umgr2wlk.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
2 umgruhgr ${⊢}{G}\in \mathrm{UMGraph}\to {G}\in \mathrm{UHGraph}$
3 1 eleq2i ${⊢}\left\{{B},{C}\right\}\in {E}↔\left\{{B},{C}\right\}\in \mathrm{Edg}\left({G}\right)$
4 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
5 4 uhgredgiedgb ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left\{{B},{C}\right\}\in \mathrm{Edg}\left({G}\right)↔\exists {i}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)$
6 3 5 syl5bb ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left\{{B},{C}\right\}\in {E}↔\exists {i}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)$
7 2 6 syl ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left\{{B},{C}\right\}\in {E}↔\exists {i}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)$
8 7 biimpd ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left\{{B},{C}\right\}\in {E}\to \exists {i}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)$
9 8 a1d ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left\{{B},{C}\right\}\in {E}\to \exists {i}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\right)$
10 9 3imp ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \exists {i}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)$
11 1 eleq2i ${⊢}\left\{{A},{B}\right\}\in {E}↔\left\{{A},{B}\right\}\in \mathrm{Edg}\left({G}\right)$
12 4 uhgredgiedgb ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left\{{A},{B}\right\}\in \mathrm{Edg}\left({G}\right)↔\exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\right)$
13 11 12 syl5bb ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left\{{A},{B}\right\}\in {E}↔\exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\right)$
14 2 13 syl ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left\{{A},{B}\right\}\in {E}↔\exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\right)$
15 14 biimpd ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left\{{A},{B}\right\}\in {E}\to \exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\right)$
16 15 a1dd ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left\{{B},{C}\right\}\in {E}\to \exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\right)\right)$
17 16 3imp ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)$
18 s2cli ${⊢}⟨“{j}{i}”⟩\in \mathrm{Word}\mathrm{V}$
19 s3cli ${⊢}⟨“{A}{B}{C}”⟩\in \mathrm{Word}\mathrm{V}$
20 18 19 pm3.2i ${⊢}\left(⟨“{j}{i}”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“{A}{B}{C}”⟩\in \mathrm{Word}\mathrm{V}\right)$
21 eqid ${⊢}⟨“{j}{i}”⟩=⟨“{j}{i}”⟩$
22 eqid ${⊢}⟨“{A}{B}{C}”⟩=⟨“{A}{B}{C}”⟩$
23 simpl1 ${⊢}\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},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\right)\to {G}\in \mathrm{UMGraph}$
24 3simpc ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)$
25 24 adantr ${⊢}\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},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\right)\to \left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)$
26 simpl ${⊢}\left(\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\to \left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)$
27 26 eqcomd ${⊢}\left(\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\to \mathrm{iEdg}\left({G}\right)\left({j}\right)=\left\{{A},{B}\right\}$
28 27 adantl ${⊢}\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},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\right)\to \mathrm{iEdg}\left({G}\right)\left({j}\right)=\left\{{A},{B}\right\}$
29 simpr ${⊢}\left(\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\to \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)$
30 29 eqcomd ${⊢}\left(\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\to \mathrm{iEdg}\left({G}\right)\left({i}\right)=\left\{{B},{C}\right\}$
31 30 adantl ${⊢}\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},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\right)\to \mathrm{iEdg}\left({G}\right)\left({i}\right)=\left\{{B},{C}\right\}$
32 1 4 21 22 23 25 28 31 umgr2adedgwlk ${⊢}\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},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\right)\to \left(⟨“{j}{i}”⟩\mathrm{Walks}\left({G}\right)⟨“{A}{B}{C}”⟩\wedge \left|⟨“{j}{i}”⟩\right|=2\wedge \left({A}=⟨“{A}{B}{C}”⟩\left(0\right)\wedge {B}=⟨“{A}{B}{C}”⟩\left(1\right)\wedge {C}=⟨“{A}{B}{C}”⟩\left(2\right)\right)\right)$
33 breq12 ${⊢}\left({f}=⟨“{j}{i}”⟩\wedge {p}=⟨“{A}{B}{C}”⟩\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}↔⟨“{j}{i}”⟩\mathrm{Walks}\left({G}\right)⟨“{A}{B}{C}”⟩\right)$
34 fveqeq2 ${⊢}{f}=⟨“{j}{i}”⟩\to \left(\left|{f}\right|=2↔\left|⟨“{j}{i}”⟩\right|=2\right)$
35 34 adantr ${⊢}\left({f}=⟨“{j}{i}”⟩\wedge {p}=⟨“{A}{B}{C}”⟩\right)\to \left(\left|{f}\right|=2↔\left|⟨“{j}{i}”⟩\right|=2\right)$
36 fveq1 ${⊢}{p}=⟨“{A}{B}{C}”⟩\to {p}\left(0\right)=⟨“{A}{B}{C}”⟩\left(0\right)$
37 36 eqeq2d ${⊢}{p}=⟨“{A}{B}{C}”⟩\to \left({A}={p}\left(0\right)↔{A}=⟨“{A}{B}{C}”⟩\left(0\right)\right)$
38 fveq1 ${⊢}{p}=⟨“{A}{B}{C}”⟩\to {p}\left(1\right)=⟨“{A}{B}{C}”⟩\left(1\right)$
39 38 eqeq2d ${⊢}{p}=⟨“{A}{B}{C}”⟩\to \left({B}={p}\left(1\right)↔{B}=⟨“{A}{B}{C}”⟩\left(1\right)\right)$
40 fveq1 ${⊢}{p}=⟨“{A}{B}{C}”⟩\to {p}\left(2\right)=⟨“{A}{B}{C}”⟩\left(2\right)$
41 40 eqeq2d ${⊢}{p}=⟨“{A}{B}{C}”⟩\to \left({C}={p}\left(2\right)↔{C}=⟨“{A}{B}{C}”⟩\left(2\right)\right)$
42 37 39 41 3anbi123d ${⊢}{p}=⟨“{A}{B}{C}”⟩\to \left(\left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)↔\left({A}=⟨“{A}{B}{C}”⟩\left(0\right)\wedge {B}=⟨“{A}{B}{C}”⟩\left(1\right)\wedge {C}=⟨“{A}{B}{C}”⟩\left(2\right)\right)\right)$
43 42 adantl ${⊢}\left({f}=⟨“{j}{i}”⟩\wedge {p}=⟨“{A}{B}{C}”⟩\right)\to \left(\left({A}={p}\left(0\right)\wedge {B}={p}\left(1\right)\wedge {C}={p}\left(2\right)\right)↔\left({A}=⟨“{A}{B}{C}”⟩\left(0\right)\wedge {B}=⟨“{A}{B}{C}”⟩\left(1\right)\wedge {C}=⟨“{A}{B}{C}”⟩\left(2\right)\right)\right)$
44 33 35 43 3anbi123d ${⊢}\left({f}=⟨“{j}{i}”⟩\wedge {p}=⟨“{A}{B}{C}”⟩\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)↔\left(⟨“{j}{i}”⟩\mathrm{Walks}\left({G}\right)⟨“{A}{B}{C}”⟩\wedge \left|⟨“{j}{i}”⟩\right|=2\wedge \left({A}=⟨“{A}{B}{C}”⟩\left(0\right)\wedge {B}=⟨“{A}{B}{C}”⟩\left(1\right)\wedge {C}=⟨“{A}{B}{C}”⟩\left(2\right)\right)\right)\right)$
45 44 spc2egv ${⊢}\left(⟨“{j}{i}”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“{A}{B}{C}”⟩\in \mathrm{Word}\mathrm{V}\right)\to \left(\left(⟨“{j}{i}”⟩\mathrm{Walks}\left({G}\right)⟨“{A}{B}{C}”⟩\wedge \left|⟨“{j}{i}”⟩\right|=2\wedge \left({A}=⟨“{A}{B}{C}”⟩\left(0\right)\wedge {B}=⟨“{A}{B}{C}”⟩\left(1\right)\wedge {C}=⟨“{A}{B}{C}”⟩\left(2\right)\right)\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)\right)$
46 20 32 45 mpsyl ${⊢}\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},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\wedge \left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\right)\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)$
47 46 exp32 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\to \left(\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\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)\right)\right)$
48 47 com12 ${⊢}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\to \left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\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)\right)\right)$
49 48 rexlimivw ${⊢}\exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\right)\to \left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\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)\right)\right)$
50 49 com13 ${⊢}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\to \left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\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)\right)\right)$
51 50 rexlimivw ${⊢}\exists {i}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\to \left(\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\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)\right)\right)$
52 51 com12 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\exists {i}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{B},{C}\right\}=\mathrm{iEdg}\left({G}\right)\left({i}\right)\to \left(\exists {j}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}=\mathrm{iEdg}\left({G}\right)\left({j}\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)\right)\right)$
53 10 17 52 mp2d ${⊢}\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)$