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 ‘ 𝐺 ) 𝑃 )