# Metamath Proof Explorer

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 ) ) ) )