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=Edg⁡G
Assertion umgr2wlk ⊢G∈UMGraph∧AB∈E∧BC∈E→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2

Proof

Step Hyp Ref Expression
1 umgr2wlk.e ⊢E=Edg⁡G
2 umgruhgr ⊢G∈UMGraph→G∈UHGraph
3 1 eleq2i ⊢BC∈E↔BC∈Edg⁡G
4 eqid ⊢iEdg⁡G=iEdg⁡G
5 4 uhgredgiedgb ⊢G∈UHGraph→BC∈Edg⁡G↔∃i∈dom⁡iEdg⁡GBC=iEdg⁡G⁡i
6 3 5 bitrid ⊢G∈UHGraph→BC∈E↔∃i∈dom⁡iEdg⁡GBC=iEdg⁡G⁡i
7 2 6 syl ⊢G∈UMGraph→BC∈E↔∃i∈dom⁡iEdg⁡GBC=iEdg⁡G⁡i
8 7 biimpd ⊢G∈UMGraph→BC∈E→∃i∈dom⁡iEdg⁡GBC=iEdg⁡G⁡i
9 8 a1d ⊢G∈UMGraph→AB∈E→BC∈E→∃i∈dom⁡iEdg⁡GBC=iEdg⁡G⁡i
10 9 3imp ⊢G∈UMGraph∧AB∈E∧BC∈E→∃i∈dom⁡iEdg⁡GBC=iEdg⁡G⁡i
11 1 eleq2i ⊢AB∈E↔AB∈Edg⁡G
12 4 uhgredgiedgb ⊢G∈UHGraph→AB∈Edg⁡G↔∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j
13 11 12 bitrid ⊢G∈UHGraph→AB∈E↔∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j
14 2 13 syl ⊢G∈UMGraph→AB∈E↔∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j
15 14 biimpd ⊢G∈UMGraph→AB∈E→∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j
16 15 a1dd ⊢G∈UMGraph→AB∈E→BC∈E→∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j
17 16 3imp ⊢G∈UMGraph∧AB∈E∧BC∈E→∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j
18 s2cli ⊢⟨“ji”⟩∈WordV
19 s3cli ⊢⟨“ABC”⟩∈WordV
20 18 19 pm3.2i ⊢⟨“ji”⟩∈WordV∧⟨“ABC”⟩∈WordV
21 eqid ⊢⟨“ji”⟩=⟨“ji”⟩
22 eqid ⊢⟨“ABC”⟩=⟨“ABC”⟩
23 simpl1 ⊢G∈UMGraph∧AB∈E∧BC∈E∧AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→G∈UMGraph
24 3simpc ⊢G∈UMGraph∧AB∈E∧BC∈E→AB∈E∧BC∈E
25 24 adantr ⊢G∈UMGraph∧AB∈E∧BC∈E∧AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→AB∈E∧BC∈E
26 simpl ⊢AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→AB=iEdg⁡G⁡j
27 26 eqcomd ⊢AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→iEdg⁡G⁡j=AB
28 27 adantl ⊢G∈UMGraph∧AB∈E∧BC∈E∧AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→iEdg⁡G⁡j=AB
29 simpr ⊢AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→BC=iEdg⁡G⁡i
30 29 eqcomd ⊢AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→iEdg⁡G⁡i=BC
31 30 adantl ⊢G∈UMGraph∧AB∈E∧BC∈E∧AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→iEdg⁡G⁡i=BC
32 1 4 21 22 23 25 28 31 umgr2adedgwlk ⊢G∈UMGraph∧AB∈E∧BC∈E∧AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→⟨“ji”⟩Walks⁡G⟨“ABC”⟩∧⟨“ji”⟩=2∧A=⟨“ABC”⟩⁡0∧B=⟨“ABC”⟩⁡1∧C=⟨“ABC”⟩⁡2
33 breq12 ⊢f=⟨“ji”⟩∧p=⟨“ABC”⟩→fWalks⁡Gp↔⟨“ji”⟩Walks⁡G⟨“ABC”⟩
34 fveqeq2 ⊢f=⟨“ji”⟩→f=2↔⟨“ji”⟩=2
35 34 adantr ⊢f=⟨“ji”⟩∧p=⟨“ABC”⟩→f=2↔⟨“ji”⟩=2
36 fveq1 ⊢p=⟨“ABC”⟩→p⁡0=⟨“ABC”⟩⁡0
37 36 eqeq2d ⊢p=⟨“ABC”⟩→A=p⁡0↔A=⟨“ABC”⟩⁡0
38 fveq1 ⊢p=⟨“ABC”⟩→p⁡1=⟨“ABC”⟩⁡1
39 38 eqeq2d ⊢p=⟨“ABC”⟩→B=p⁡1↔B=⟨“ABC”⟩⁡1
40 fveq1 ⊢p=⟨“ABC”⟩→p⁡2=⟨“ABC”⟩⁡2
41 40 eqeq2d ⊢p=⟨“ABC”⟩→C=p⁡2↔C=⟨“ABC”⟩⁡2
42 37 39 41 3anbi123d ⊢p=⟨“ABC”⟩→A=p⁡0∧B=p⁡1∧C=p⁡2↔A=⟨“ABC”⟩⁡0∧B=⟨“ABC”⟩⁡1∧C=⟨“ABC”⟩⁡2
43 42 adantl ⊢f=⟨“ji”⟩∧p=⟨“ABC”⟩→A=p⁡0∧B=p⁡1∧C=p⁡2↔A=⟨“ABC”⟩⁡0∧B=⟨“ABC”⟩⁡1∧C=⟨“ABC”⟩⁡2
44 33 35 43 3anbi123d ⊢f=⟨“ji”⟩∧p=⟨“ABC”⟩→fWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2↔⟨“ji”⟩Walks⁡G⟨“ABC”⟩∧⟨“ji”⟩=2∧A=⟨“ABC”⟩⁡0∧B=⟨“ABC”⟩⁡1∧C=⟨“ABC”⟩⁡2
45 44 spc2egv ⊢⟨“ji”⟩∈WordV∧⟨“ABC”⟩∈WordV→⟨“ji”⟩Walks⁡G⟨“ABC”⟩∧⟨“ji”⟩=2∧A=⟨“ABC”⟩⁡0∧B=⟨“ABC”⟩⁡1∧C=⟨“ABC”⟩⁡2→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2
46 20 32 45 mpsyl ⊢G∈UMGraph∧AB∈E∧BC∈E∧AB=iEdg⁡G⁡j∧BC=iEdg⁡G⁡i→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2
47 46 exp32 ⊢G∈UMGraph∧AB∈E∧BC∈E→AB=iEdg⁡G⁡j→BC=iEdg⁡G⁡i→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2
48 47 com12 ⊢AB=iEdg⁡G⁡j→G∈UMGraph∧AB∈E∧BC∈E→BC=iEdg⁡G⁡i→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2
49 48 rexlimivw ⊢∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j→G∈UMGraph∧AB∈E∧BC∈E→BC=iEdg⁡G⁡i→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2
50 49 com13 ⊢BC=iEdg⁡G⁡i→G∈UMGraph∧AB∈E∧BC∈E→∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2
51 50 rexlimivw ⊢∃i∈dom⁡iEdg⁡GBC=iEdg⁡G⁡i→G∈UMGraph∧AB∈E∧BC∈E→∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2
52 51 com12 ⊢G∈UMGraph∧AB∈E∧BC∈E→∃i∈dom⁡iEdg⁡GBC=iEdg⁡G⁡i→∃j∈dom⁡iEdg⁡GAB=iEdg⁡G⁡j→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2
53 10 17 52 mp2d ⊢G∈UMGraph∧AB∈E∧BC∈E→∃f∃pfWalks⁡Gp∧f=2∧A=p⁡0∧B=p⁡1∧C=p⁡2