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