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 = Edg ⁡ G
Assertion umgr2wlkon ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → ∃ f ∃ p f A WalksOn ⁡ G C p

Proof

Step Hyp Ref Expression
1 umgr2wlk.e ⊢ E = Edg ⁡ G
2 1 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
3 simp1 ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p
4 eqcom ⊢ A = p ⁡ 0 ↔ p ⁡ 0 = A
5 4 biimpi ⊢ A = p ⁡ 0 → p ⁡ 0 = A
6 5 3ad2ant1 ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ 0 = A
7 6 3ad2ant3 ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ 0 = A
8 fveq2 ⊢ 2 = f → p ⁡ 2 = p ⁡ f
9 8 eqcoms ⊢ f = 2 → p ⁡ 2 = p ⁡ f
10 9 eqeq1d ⊢ f = 2 → p ⁡ 2 = C ↔ p ⁡ f = C
11 10 biimpcd ⊢ p ⁡ 2 = C → f = 2 → p ⁡ f = C
12 11 eqcoms ⊢ C = p ⁡ 2 → f = 2 → p ⁡ f = C
13 12 3ad2ant3 ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f = 2 → p ⁡ f = C
14 13 com12 ⊢ f = 2 → A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ f = C
15 14 a1i ⊢ f Walks ⁡ G p → f = 2 → A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ f = C
16 15 3imp ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ f = C
17 3 7 16 3jca ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p ∧ p ⁡ 0 = A ∧ p ⁡ f = C
18 17 adantl ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p ∧ p ⁡ 0 = A ∧ p ⁡ f = C
19 1 umgr2adedgwlklem ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
20 simprr1 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G
21 simprr3 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → C ∈ Vtx ⁡ G
22 20 21 jca ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
23 19 22 mpdan ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
24 vex ⊢ f ∈ V
25 vex ⊢ p ∈ V
26 24 25 pm3.2i ⊢ f ∈ V ∧ p ∈ V
27 26 a1i ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f ∈ V ∧ p ∈ V
28 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
29 28 iswlkon ⊢ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G ∧ f ∈ V ∧ p ∈ V → f A WalksOn ⁡ G C p ↔ f Walks ⁡ G p ∧ p ⁡ 0 = A ∧ p ⁡ f = C
30 23 27 29 syl2an2r ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f A WalksOn ⁡ G C p ↔ f Walks ⁡ G p ∧ p ⁡ 0 = A ∧ p ⁡ f = C
31 18 30 mpbird ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f A WalksOn ⁡ G C p
32 31 ex ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f A WalksOn ⁡ G C p
33 32 2eximdv ⊢ 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 → ∃ f ∃ p f A WalksOn ⁡ G C p
34 2 33 mpd ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → ∃ f ∃ p f A WalksOn ⁡ G C p