Metamath Proof Explorer

Theorem umgr2adedgwlkonALT

Description: Alternate proof for umgr2adedgwlkon , using umgr2adedgwlk , but with a much longer proof! In a multigraph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 30-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses umgr2adedgwlk.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
umgr2adedgwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
umgr2adedgwlk.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
umgr2adedgwlk.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
umgr2adedgwlk.g ⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
umgr2adedgwlk.a ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
umgr2adedgwlk.j ⊢ ( 𝜑 → ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } )
umgr2adedgwlk.k ⊢ ( 𝜑 → ( 𝐼 ‘ 𝐾 ) = { 𝐵 , 𝐶 } )
Assertion umgr2adedgwlkonALT ( 𝜑 → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 )

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 1 2 3 4 5 6 7 8 umgr2adedgwlk ⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) )
10 simp1 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
11 id ⊢ ( ( 𝑃 ‘ 0 ) = 𝐴 → ( 𝑃 ‘ 0 ) = 𝐴 )
12 11 eqcoms ⊢ ( 𝐴 = ( 𝑃 ‘ 0 ) → ( 𝑃 ‘ 0 ) = 𝐴 )
13 12 3ad2ant1 ⊢ ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ 0 ) = 𝐴 )
14 13 3ad2ant3 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) → ( 𝑃 ‘ 0 ) = 𝐴 )
15 fveq2 ⊢ ( 2 = ( ♯ ‘ 𝐹 ) → ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
16 15 eqcoms ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
17 16 eqeq1d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝑃 ‘ 2 ) = 𝐶 ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) )
18 17 biimpcd ⊢ ( ( 𝑃 ‘ 2 ) = 𝐶 → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) )
19 18 eqcoms ⊢ ( 𝐶 = ( 𝑃 ‘ 2 ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) )
20 19 3ad2ant3 ⊢ ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) )
21 20 com12 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) )
22 21 a1i ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) )
23 22 3imp ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 )
24 10 14 23 3jca ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) )
25 9 24 syl ⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) )
26 3anass ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐺 ∈ UMGraph ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
27 5 6 26 sylanbrc ⊢ ( 𝜑 → ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
28 1 umgr2adedgwlklem ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
29 3simpb ⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
30 29 adantl ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
31 27 28 30 3syl ⊢ ( 𝜑 → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
32 3anass ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ↔ ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
33 5 31 32 sylanbrc ⊢ ( 𝜑 → ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
34 s2cli ⊢ ⟨“ 𝐽 𝐾 ”⟩ ∈ Word V
35 3 34 eqeltri ⊢ 𝐹 ∈ Word V
36 s3cli ⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V
37 4 36 eqeltri ⊢ 𝑃 ∈ Word V
38 35 37 pm3.2i ⊢ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V )
39 id ⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
40 39 3adant1 ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
41 40 anim1i ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) )
42 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
43 42 iswlkon ⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) )
44 41 43 syl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) )
45 33 38 44 sylancl ⊢ ( 𝜑 → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) )
46 25 45 mpbird ⊢ ( 𝜑 → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 )