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 ∧ A B ∈ E ∧ B C ∈ E → ∃ f ∃ p f Walks ⁡ G p ∧ 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 ⊢ B C ∈ E ↔ B C ∈ Edg ⁡ G
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 4 uhgredgiedgb ⊢ G ∈ UHGraph → B C ∈ Edg ⁡ G ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ i
6 3 5 bitrid ⊢ G ∈ UHGraph → B C ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ i
7 2 6 syl ⊢ G ∈ UMGraph → B C ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ i
8 7 biimpd ⊢ G ∈ UMGraph → B C ∈ E → ∃ i ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ i
9 8 a1d ⊢ G ∈ UMGraph → A B ∈ E → B C ∈ E → ∃ i ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ i
10 9 3imp ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → ∃ i ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ i
11 1 eleq2i ⊢ A B ∈ E ↔ A B ∈ Edg ⁡ G
12 4 uhgredgiedgb ⊢ G ∈ UHGraph → A B ∈ Edg ⁡ G ↔ ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j
13 11 12 bitrid ⊢ G ∈ UHGraph → A B ∈ E ↔ ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j
14 2 13 syl ⊢ G ∈ UMGraph → A B ∈ E ↔ ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j
15 14 biimpd ⊢ G ∈ UMGraph → A B ∈ E → ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j
16 15 a1dd ⊢ G ∈ UMGraph → A B ∈ E → B C ∈ E → ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j
17 16 3imp ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j
18 s2cli ⊢ ⟨“ ji ”⟩ ∈ Word V
19 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
20 18 19 pm3.2i ⊢ ⟨“ ji ”⟩ ∈ Word V ∧ ⟨“ ABC ”⟩ ∈ Word V
21 eqid ⊢ ⟨“ ji ”⟩ = ⟨“ ji ”⟩
22 eqid ⊢ ⟨“ ABC ”⟩ = ⟨“ ABC ”⟩
23 simpl1 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → G ∈ UMGraph
24 3simpc ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A B ∈ E ∧ B C ∈ E
25 24 adantr ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → A B ∈ E ∧ B C ∈ E
26 simpl ⊢ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → A B = iEdg ⁡ G ⁡ j
27 26 eqcomd ⊢ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → iEdg ⁡ G ⁡ j = A B
28 27 adantl ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → iEdg ⁡ G ⁡ j = A B
29 simpr ⊢ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → B C = iEdg ⁡ G ⁡ i
30 29 eqcomd ⊢ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → iEdg ⁡ G ⁡ i = B C
31 30 adantl ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → iEdg ⁡ G ⁡ i = B C
32 1 4 21 22 23 25 28 31 umgr2adedgwlk ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → ⟨“ ji ”⟩ Walks ⁡ G ⟨“ ABC ”⟩ ∧ ⟨“ ji ”⟩ = 2 ∧ A = ⟨“ ABC ”⟩ ⁡ 0 ∧ B = ⟨“ ABC ”⟩ ⁡ 1 ∧ C = ⟨“ ABC ”⟩ ⁡ 2
33 breq12 ⊢ f = ⟨“ ji ”⟩ ∧ p = ⟨“ ABC ”⟩ → f Walks ⁡ G p ↔ ⟨“ 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 ”⟩ → f Walks ⁡ G p ∧ 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 ”⟩ ∈ Word V ∧ ⟨“ ABC ”⟩ ∈ Word V → ⟨“ ji ”⟩ Walks ⁡ G ⟨“ ABC ”⟩ ∧ ⟨“ ji ”⟩ = 2 ∧ A = ⟨“ ABC ”⟩ ⁡ 0 ∧ B = ⟨“ ABC ”⟩ ⁡ 1 ∧ C = ⟨“ ABC ”⟩ ⁡ 2 → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2
46 20 32 45 mpsyl ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A B = iEdg ⁡ G ⁡ j ∧ B C = iEdg ⁡ G ⁡ i → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2
47 46 exp32 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A B = iEdg ⁡ G ⁡ j → B C = iEdg ⁡ G ⁡ i → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2
48 47 com12 ⊢ A B = iEdg ⁡ G ⁡ j → G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → B C = iEdg ⁡ G ⁡ i → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2
49 48 rexlimivw ⊢ ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j → G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → B C = iEdg ⁡ G ⁡ i → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2
50 49 com13 ⊢ B C = iEdg ⁡ G ⁡ i → G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2
51 50 rexlimivw ⊢ ∃ i ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ i → G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2
52 51 com12 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → ∃ i ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ i → ∃ j ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ j → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2
53 10 17 52 mp2d ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → ∃ f ∃ p f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2