Metamath Proof Explorer

Theorem umgr2adedgwlk

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 = 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 umgr2adedgwlk ⊢ φ → F Walks ⁡ G P ∧ F = 2 ∧ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2

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 2wlkd ⊢ φ → F Walks ⁡ G P
22 3 fveq2i ⊢ F = ⟨“ JK ”⟩
23 s2len ⊢ ⟨“ JK ”⟩ = 2
24 22 23 eqtri ⊢ F = 2
25 24 a1i ⊢ φ → F = 2
26 s3fv0 ⊢ A ∈ Vtx ⁡ G → ⟨“ ABC ”⟩ ⁡ 0 = A
27 s3fv1 ⊢ B ∈ Vtx ⁡ G → ⟨“ ABC ”⟩ ⁡ 1 = B
28 s3fv2 ⊢ C ∈ Vtx ⁡ G → ⟨“ ABC ”⟩ ⁡ 2 = C
29 26 27 28 3anim123i ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 1 = B ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
30 13 29 syl ⊢ φ → ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 1 = B ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
31 4 fveq1i ⊢ P ⁡ 0 = ⟨“ ABC ”⟩ ⁡ 0
32 31 eqeq2i ⊢ A = P ⁡ 0 ↔ A = ⟨“ ABC ”⟩ ⁡ 0
33 eqcom ⊢ A = ⟨“ ABC ”⟩ ⁡ 0 ↔ ⟨“ ABC ”⟩ ⁡ 0 = A
34 32 33 bitri ⊢ A = P ⁡ 0 ↔ ⟨“ ABC ”⟩ ⁡ 0 = A
35 4 fveq1i ⊢ P ⁡ 1 = ⟨“ ABC ”⟩ ⁡ 1
36 35 eqeq2i ⊢ B = P ⁡ 1 ↔ B = ⟨“ ABC ”⟩ ⁡ 1
37 eqcom ⊢ B = ⟨“ ABC ”⟩ ⁡ 1 ↔ ⟨“ ABC ”⟩ ⁡ 1 = B
38 36 37 bitri ⊢ B = P ⁡ 1 ↔ ⟨“ ABC ”⟩ ⁡ 1 = B
39 4 fveq1i ⊢ P ⁡ 2 = ⟨“ ABC ”⟩ ⁡ 2
40 39 eqeq2i ⊢ C = P ⁡ 2 ↔ C = ⟨“ ABC ”⟩ ⁡ 2
41 eqcom ⊢ C = ⟨“ ABC ”⟩ ⁡ 2 ↔ ⟨“ ABC ”⟩ ⁡ 2 = C
42 40 41 bitri ⊢ C = P ⁡ 2 ↔ ⟨“ ABC ”⟩ ⁡ 2 = C
43 34 38 42 3anbi123i ⊢ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 ↔ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 1 = B ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
44 30 43 sylibr ⊢ φ → A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2
45 21 25 44 3jca ⊢ φ → F Walks ⁡ G P ∧ F = 2 ∧ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2