Metamath Proof Explorer

Theorem umgr2adedgspth

Description: In a multigraph, two adjacent edges with different endvertices form a simple path of length 2. (Contributed by Alexander van der Vekens, 1-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
umgr2adedgspth.n ⊢ φ → A ≠ C
Assertion umgr2adedgspth ⊢ φ → F SPaths ⁡ G 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 umgr2adedgspth.n ⊢ φ → A ≠ C
10 3anass ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ↔ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E
11 5 6 10 sylanbrc ⊢ φ → G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E
12 1 umgr2adedgwlklem ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
13 11 12 syl ⊢ φ → A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
14 13 simprd ⊢ φ → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
15 13 simpld ⊢ φ → A ≠ B ∧ B ≠ C
16 ssid ⊢ A B ⊆ A B
17 16 7 sseqtrrid ⊢ φ → A B ⊆ I ⁡ J
18 ssid ⊢ B C ⊆ B C
19 18 8 sseqtrrid ⊢ φ → B C ⊆ I ⁡ K
20 17 19 jca ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
21 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
22 fveq2 ⊢ K = J → I ⁡ K = I ⁡ J
23 22 eqcoms ⊢ J = K → I ⁡ K = I ⁡ J
24 23 eqeq1d ⊢ J = K → I ⁡ K = B C ↔ I ⁡ J = B C
25 eqtr2 ⊢ I ⁡ J = B C ∧ I ⁡ J = A B → B C = A B
26 25 ex ⊢ I ⁡ J = B C → I ⁡ J = A B → B C = A B
27 24 26 syl6bi ⊢ J = K → I ⁡ K = B C → I ⁡ J = A B → B C = A B
28 27 com13 ⊢ I ⁡ J = A B → I ⁡ K = B C → J = K → B C = A B
29 7 8 28 sylc ⊢ φ → J = K → B C = A B
30 eqcom ⊢ B C = A B ↔ A B = B C
31 prcom ⊢ B C = C B
32 31 eqeq2i ⊢ A B = B C ↔ A B = C B
33 30 32 bitri ⊢ B C = A B ↔ A B = C B
34 21 1 umgrpredgv ⊢ G ∈ UMGraph ∧ A B ∈ E → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
35 34 simpld ⊢ G ∈ UMGraph ∧ A B ∈ E → A ∈ Vtx ⁡ G
36 35 ex ⊢ G ∈ UMGraph → A B ∈ E → A ∈ Vtx ⁡ G
37 21 1 umgrpredgv ⊢ G ∈ UMGraph ∧ B C ∈ E → B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
38 37 simprd ⊢ G ∈ UMGraph ∧ B C ∈ E → C ∈ Vtx ⁡ G
39 38 ex ⊢ G ∈ UMGraph → B C ∈ E → C ∈ Vtx ⁡ G
40 36 39 anim12d ⊢ G ∈ UMGraph → A B ∈ E ∧ B C ∈ E → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
41 5 6 40 sylc ⊢ φ → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
42 preqr1g ⊢ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → A B = C B → A = C
43 41 42 syl ⊢ φ → A B = C B → A = C
44 eqneqall ⊢ A = C → A ≠ C → J ≠ K
45 43 9 44 syl6ci ⊢ φ → A B = C B → J ≠ K
46 33 45 syl5bi ⊢ φ → B C = A B → J ≠ K
47 29 46 syld ⊢ φ → J = K → J ≠ K
48 neqne ⊢ ¬ J = K → J ≠ K
49 47 48 pm2.61d1 ⊢ φ → J ≠ K
50 4 3 14 15 20 21 2 49 9 2spthd ⊢ φ → F SPaths ⁡ G P