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

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		3anass	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐺 ∈ UMGraph ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
10	5 6 9	sylanbrc	⊢ ( 𝜑 → ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
11	1	umgr2adedgwlklem	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
12	10 11	syl	⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
13	12	simprd	⊢ ( 𝜑 → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
14	12	simpld	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
15		ssid	⊢ { 𝐴 , 𝐵 } ⊆ { 𝐴 , 𝐵 }
16	15 7	sseqtrrid	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) )
17		ssid	⊢ { 𝐵 , 𝐶 } ⊆ { 𝐵 , 𝐶 }
18	17 8	sseqtrrid	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) )
19	16 18	jca	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
20		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
21	4 3 13 14 19 20 2	2wlkd	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
22	3	fveq2i	⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 𝐾 ”⟩ )
23		s2len	⊢ ( ♯ ‘ ⟨“ 𝐽 𝐾 ”⟩ ) = 2
24	22 23	eqtri	⊢ ( ♯ ‘ 𝐹 ) = 2
25	24	a1i	⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = 2 )
26		s3fv0	⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
27		s3fv1	⊢ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
28		s3fv2	⊢ ( 𝐶 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
29	26 27 28	3anim123i	⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) )
30	13 29	syl	⊢ ( 𝜑 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) )
31	4	fveq1i	⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 )
32	31	eqeq2i	⊢ ( 𝐴 = ( 𝑃 ‘ 0 ) ↔ 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) )
33		eqcom	⊢ ( 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
34	32 33	bitri	⊢ ( 𝐴 = ( 𝑃 ‘ 0 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
35	4	fveq1i	⊢ ( 𝑃 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 )
36	35	eqeq2i	⊢ ( 𝐵 = ( 𝑃 ‘ 1 ) ↔ 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
37		eqcom	⊢ ( 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
38	36 37	bitri	⊢ ( 𝐵 = ( 𝑃 ‘ 1 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
39	4	fveq1i	⊢ ( 𝑃 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 )
40	39	eqeq2i	⊢ ( 𝐶 = ( 𝑃 ‘ 2 ) ↔ 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
41		eqcom	⊢ ( 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
42	40 41	bitri	⊢ ( 𝐶 = ( 𝑃 ‘ 2 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
43	34 38 42	3anbi123i	⊢ ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) )
44	30 43	sylibr	⊢ ( 𝜑 → ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) )
45	21 25 44	3jca	⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) )

Metamath Proof Explorer

Theorem umgr2adedgwlk

Proof