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 𝐸 = ( Edg ‘ 𝐺 )
umgr2adedgwlk.i 𝐼 = ( iEdg ‘ 𝐺 )
umgr2adedgwlk.f 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
umgr2adedgwlk.p 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
umgr2adedgwlk.g ( 𝜑𝐺 ∈ UMGraph )
umgr2adedgwlk.a ( 𝜑 → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
umgr2adedgwlk.j ( 𝜑 → ( 𝐼𝐽 ) = { 𝐴 , 𝐵 } )
umgr2adedgwlk.k ( 𝜑 → ( 𝐼𝐾 ) = { 𝐵 , 𝐶 } )
umgr2adedgspth.n ( 𝜑𝐴𝐶 )
Assertion umgr2adedgspth ( 𝜑𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e 𝐸 = ( Edg ‘ 𝐺 )
2 umgr2adedgwlk.i 𝐼 = ( iEdg ‘ 𝐺 )
3 umgr2adedgwlk.f 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
4 umgr2adedgwlk.p 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
5 umgr2adedgwlk.g ( 𝜑𝐺 ∈ UMGraph )
6 umgr2adedgwlk.a ( 𝜑 → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
7 umgr2adedgwlk.j ( 𝜑 → ( 𝐼𝐽 ) = { 𝐴 , 𝐵 } )
8 umgr2adedgwlk.k ( 𝜑 → ( 𝐼𝐾 ) = { 𝐵 , 𝐶 } )
9 umgr2adedgspth.n ( 𝜑𝐴𝐶 )
10 3anass ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐺 ∈ UMGraph ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
11 5 6 10 sylanbrc ( 𝜑 → ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
12 1 umgr2adedgwlklem ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
13 11 12 syl ( 𝜑 → ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
14 13 simprd ( 𝜑 → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
15 13 simpld ( 𝜑 → ( 𝐴𝐵𝐵𝐶 ) )
16 ssid { 𝐴 , 𝐵 } ⊆ { 𝐴 , 𝐵 }
17 16 7 sseqtrrid ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ( 𝐼𝐽 ) )
18 ssid { 𝐵 , 𝐶 } ⊆ { 𝐵 , 𝐶 }
19 18 8 sseqtrrid ( 𝜑 → { 𝐵 , 𝐶 } ⊆ ( 𝐼𝐾 ) )
20 17 19 jca ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼𝐾 ) ) )
21 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
22 fveq2 ( 𝐾 = 𝐽 → ( 𝐼𝐾 ) = ( 𝐼𝐽 ) )
23 22 eqcoms ( 𝐽 = 𝐾 → ( 𝐼𝐾 ) = ( 𝐼𝐽 ) )
24 23 eqeq1d ( 𝐽 = 𝐾 → ( ( 𝐼𝐾 ) = { 𝐵 , 𝐶 } ↔ ( 𝐼𝐽 ) = { 𝐵 , 𝐶 } ) )
25 eqtr2 ( ( ( 𝐼𝐽 ) = { 𝐵 , 𝐶 } ∧ ( 𝐼𝐽 ) = { 𝐴 , 𝐵 } ) → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
26 25 ex ( ( 𝐼𝐽 ) = { 𝐵 , 𝐶 } → ( ( 𝐼𝐽 ) = { 𝐴 , 𝐵 } → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) )
27 24 26 syl6bi ( 𝐽 = 𝐾 → ( ( 𝐼𝐾 ) = { 𝐵 , 𝐶 } → ( ( 𝐼𝐽 ) = { 𝐴 , 𝐵 } → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) ) )
28 27 com13 ( ( 𝐼𝐽 ) = { 𝐴 , 𝐵 } → ( ( 𝐼𝐾 ) = { 𝐵 , 𝐶 } → ( 𝐽 = 𝐾 → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) ) )
29 7 8 28 sylc ( 𝜑 → ( 𝐽 = 𝐾 → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) )
30 eqcom ( { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } )
31 prcom { 𝐵 , 𝐶 } = { 𝐶 , 𝐵 }
32 31 eqeq2i ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ↔ { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } )
33 30 32 bitri ( { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } )
34 21 1 umgrpredgv ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
35 34 simpld ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
36 35 ex ( 𝐺 ∈ UMGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
37 21 1 umgrpredgv ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
38 37 simprd ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
39 38 ex ( 𝐺 ∈ UMGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
40 36 39 anim12d ( 𝐺 ∈ UMGraph → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
41 5 6 40 sylc ( 𝜑 → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
42 preqr1g ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } → 𝐴 = 𝐶 ) )
43 41 42 syl ( 𝜑 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } → 𝐴 = 𝐶 ) )
44 eqneqall ( 𝐴 = 𝐶 → ( 𝐴𝐶𝐽𝐾 ) )
45 43 9 44 syl6ci ( 𝜑 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } → 𝐽𝐾 ) )
46 33 45 syl5bi ( 𝜑 → ( { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } → 𝐽𝐾 ) )
47 29 46 syld ( 𝜑 → ( 𝐽 = 𝐾𝐽𝐾 ) )
48 neqne ( ¬ 𝐽 = 𝐾𝐽𝐾 )
49 47 48 pm2.61d1 ( 𝜑𝐽𝐾 )
50 4 3 14 15 20 21 2 49 9 2spthd ( 𝜑𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )