Metamath Proof Explorer

Theorem umgr2adedgwlkon

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

Ref Expression
Hypotheses umgr2adedgwlk.e ⊢ E = Edg ⁡ G
umgr2adedgwlk.i ⊢ I = iEdg ⁡ G
umgr2adedgwlk.f ⊢ F = ⟨“ JK ”⟩
umgr2adedgwlk.p ⊢ P = ⟨“ ABC ”⟩
umgr2adedgwlk.g ⊢ φ → G ∈ UMGraph
umgr2adedgwlk.a ⊢ φ → A B ∈ E ∧ B C ∈ E
umgr2adedgwlk.j ⊢ φ → I ⁡ J = A B
umgr2adedgwlk.k ⊢ φ → I ⁡ K = B C
Assertion umgr2adedgwlkon ⊢ φ → F A WalksOn ⁡ G C P

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e ⊢ E = Edg ⁡ G
2 umgr2adedgwlk.i ⊢ I = iEdg ⁡ G
3 umgr2adedgwlk.f ⊢ F = ⟨“ JK ”⟩
4 umgr2adedgwlk.p ⊢ P = ⟨“ ABC ”⟩
5 umgr2adedgwlk.g ⊢ φ → G ∈ UMGraph
6 umgr2adedgwlk.a ⊢ φ → A B ∈ E ∧ B C ∈ E
7 umgr2adedgwlk.j ⊢ φ → I ⁡ J = A B
8 umgr2adedgwlk.k ⊢ φ → I ⁡ K = B C
9 3anass ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ↔ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E
10 5 6 9 sylanbrc ⊢ φ → G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E
11 1 umgr2adedgwlklem ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
12 10 11 syl ⊢ φ → A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
13 12 simprd ⊢ φ → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
14 12 simpld ⊢ φ → A ≠ B ∧ B ≠ C
15 ssid ⊢ A B ⊆ A B
16 15 7 sseqtrrid ⊢ φ → A B ⊆ I ⁡ J
17 ssid ⊢ B C ⊆ B C
18 17 8 sseqtrrid ⊢ φ → B C ⊆ I ⁡ K
19 16 18 jca ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
20 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
21 4 3 13 14 19 20 2 2wlkond ⊢ φ → F A WalksOn ⁡ G C P