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