# Metamath Proof Explorer

Description: In a multigraph, two adjacent edges form a walk of length 2. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 29-Jan-2021)

Ref Expression
Hypotheses umgr2adedgwlk.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
umgr2adedgwlk.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
umgr2adedgwlk.f ${⊢}{F}=⟨“{J}{K}”⟩$
umgr2adedgwlk.p ${⊢}{P}=⟨“{A}{B}{C}”⟩$
umgr2adedgwlk.g ${⊢}{\phi }\to {G}\in \mathrm{UMGraph}$
umgr2adedgwlk.a ${⊢}{\phi }\to \left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)$
umgr2adedgwlk.j ${⊢}{\phi }\to {I}\left({J}\right)=\left\{{A},{B}\right\}$
umgr2adedgwlk.k ${⊢}{\phi }\to {I}\left({K}\right)=\left\{{B},{C}\right\}$
Assertion umgr2adedgwlk ${⊢}{\phi }\to \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 umgr2adedgwlk.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
2 umgr2adedgwlk.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 umgr2adedgwlk.f ${⊢}{F}=⟨“{J}{K}”⟩$
4 umgr2adedgwlk.p ${⊢}{P}=⟨“{A}{B}{C}”⟩$
5 umgr2adedgwlk.g ${⊢}{\phi }\to {G}\in \mathrm{UMGraph}$
6 umgr2adedgwlk.a ${⊢}{\phi }\to \left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)$
7 umgr2adedgwlk.j ${⊢}{\phi }\to {I}\left({J}\right)=\left\{{A},{B}\right\}$
8 umgr2adedgwlk.k ${⊢}{\phi }\to {I}\left({K}\right)=\left\{{B},{C}\right\}$
9 3anass ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)↔\left({G}\in \mathrm{UMGraph}\wedge \left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
10 5 6 9 sylanbrc ${⊢}{\phi }\to \left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)$
11 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)$
12 10 11 syl ${⊢}{\phi }\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)$
13 12 simprd ${⊢}{\phi }\to \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)$
14 12 simpld ${⊢}{\phi }\to \left({A}\ne {B}\wedge {B}\ne {C}\right)$
15 ssid ${⊢}\left\{{A},{B}\right\}\subseteq \left\{{A},{B}\right\}$
16 15 7 sseqtrrid ${⊢}{\phi }\to \left\{{A},{B}\right\}\subseteq {I}\left({J}\right)$
17 ssid ${⊢}\left\{{B},{C}\right\}\subseteq \left\{{B},{C}\right\}$
18 17 8 sseqtrrid ${⊢}{\phi }\to \left\{{B},{C}\right\}\subseteq {I}\left({K}\right)$
19 16 18 jca ${⊢}{\phi }\to \left(\left\{{A},{B}\right\}\subseteq {I}\left({J}\right)\wedge \left\{{B},{C}\right\}\subseteq {I}\left({K}\right)\right)$
20 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
21 4 3 13 14 19 20 2 2wlkd ${⊢}{\phi }\to {F}\mathrm{Walks}\left({G}\right){P}$
22 3 fveq2i ${⊢}\left|{F}\right|=\left|⟨“{J}{K}”⟩\right|$
23 s2len ${⊢}\left|⟨“{J}{K}”⟩\right|=2$
24 22 23 eqtri ${⊢}\left|{F}\right|=2$
25 24 a1i ${⊢}{\phi }\to \left|{F}\right|=2$
26 s3fv0 ${⊢}{A}\in \mathrm{Vtx}\left({G}\right)\to ⟨“{A}{B}{C}”⟩\left(0\right)={A}$
27 s3fv1 ${⊢}{B}\in \mathrm{Vtx}\left({G}\right)\to ⟨“{A}{B}{C}”⟩\left(1\right)={B}$
28 s3fv2 ${⊢}{C}\in \mathrm{Vtx}\left({G}\right)\to ⟨“{A}{B}{C}”⟩\left(2\right)={C}$
29 26 27 28 3anim123i ${⊢}\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)\to \left(⟨“{A}{B}{C}”⟩\left(0\right)={A}\wedge ⟨“{A}{B}{C}”⟩\left(1\right)={B}\wedge ⟨“{A}{B}{C}”⟩\left(2\right)={C}\right)$
30 13 29 syl ${⊢}{\phi }\to \left(⟨“{A}{B}{C}”⟩\left(0\right)={A}\wedge ⟨“{A}{B}{C}”⟩\left(1\right)={B}\wedge ⟨“{A}{B}{C}”⟩\left(2\right)={C}\right)$
31 4 fveq1i ${⊢}{P}\left(0\right)=⟨“{A}{B}{C}”⟩\left(0\right)$
32 31 eqeq2i ${⊢}{A}={P}\left(0\right)↔{A}=⟨“{A}{B}{C}”⟩\left(0\right)$
33 eqcom ${⊢}{A}=⟨“{A}{B}{C}”⟩\left(0\right)↔⟨“{A}{B}{C}”⟩\left(0\right)={A}$
34 32 33 bitri ${⊢}{A}={P}\left(0\right)↔⟨“{A}{B}{C}”⟩\left(0\right)={A}$
35 4 fveq1i ${⊢}{P}\left(1\right)=⟨“{A}{B}{C}”⟩\left(1\right)$
36 35 eqeq2i ${⊢}{B}={P}\left(1\right)↔{B}=⟨“{A}{B}{C}”⟩\left(1\right)$
37 eqcom ${⊢}{B}=⟨“{A}{B}{C}”⟩\left(1\right)↔⟨“{A}{B}{C}”⟩\left(1\right)={B}$
38 36 37 bitri ${⊢}{B}={P}\left(1\right)↔⟨“{A}{B}{C}”⟩\left(1\right)={B}$
39 4 fveq1i ${⊢}{P}\left(2\right)=⟨“{A}{B}{C}”⟩\left(2\right)$
40 39 eqeq2i ${⊢}{C}={P}\left(2\right)↔{C}=⟨“{A}{B}{C}”⟩\left(2\right)$
41 eqcom ${⊢}{C}=⟨“{A}{B}{C}”⟩\left(2\right)↔⟨“{A}{B}{C}”⟩\left(2\right)={C}$
42 40 41 bitri ${⊢}{C}={P}\left(2\right)↔⟨“{A}{B}{C}”⟩\left(2\right)={C}$
43 34 38 42 3anbi123i ${⊢}\left({A}={P}\left(0\right)\wedge {B}={P}\left(1\right)\wedge {C}={P}\left(2\right)\right)↔\left(⟨“{A}{B}{C}”⟩\left(0\right)={A}\wedge ⟨“{A}{B}{C}”⟩\left(1\right)={B}\wedge ⟨“{A}{B}{C}”⟩\left(2\right)={C}\right)$
44 30 43 sylibr ${⊢}{\phi }\to \left({A}={P}\left(0\right)\wedge {B}={P}\left(1\right)\wedge {C}={P}\left(2\right)\right)$
45 21 25 44 3jca ${⊢}{\phi }\to \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)$