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
|- E = ( Edg ` G )
umgr2adedgwlk.i
|- I = ( iEdg ` G )
umgr2adedgwlk.f
|- F = <" J K ">
umgr2adedgwlk.p
|- P = <" A B C ">
umgr2adedgwlk.g
|- ( ph -> G e. UMGraph )
umgr2adedgwlk.a
|- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )
umgr2adedgwlk.j
|- ( ph -> ( I ` J ) = { A , B } )
umgr2adedgwlk.k
|- ( ph -> ( I ` K ) = { B , C } )
Assertion umgr2adedgwlkonALT
|- ( ph -> F ( A ( WalksOn ` G ) C ) P )

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e
 |-  E = ( Edg ` G )
2 umgr2adedgwlk.i
 |-  I = ( iEdg ` G )
3 umgr2adedgwlk.f
 |-  F = <" J K ">
4 umgr2adedgwlk.p
 |-  P = <" A B C ">
5 umgr2adedgwlk.g
 |-  ( ph -> G e. UMGraph )
6 umgr2adedgwlk.a
 |-  ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )
7 umgr2adedgwlk.j
 |-  ( ph -> ( I ` J ) = { A , B } )
8 umgr2adedgwlk.k
 |-  ( ph -> ( I ` K ) = { B , C } )
9 1 2 3 4 5 6 7 8 umgr2adedgwlk
 |-  ( ph -> ( F ( Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) )
10 simp1
 |-  ( ( F ( Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) -> F ( Walks ` G ) P )
11 id
 |-  ( ( P ` 0 ) = A -> ( P ` 0 ) = A )
12 11 eqcoms
 |-  ( A = ( P ` 0 ) -> ( P ` 0 ) = A )
13 12 3ad2ant1
 |-  ( ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) -> ( P ` 0 ) = A )
14 13 3ad2ant3
 |-  ( ( F ( Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) -> ( P ` 0 ) = A )
15 fveq2
 |-  ( 2 = ( # ` F ) -> ( P ` 2 ) = ( P ` ( # ` F ) ) )
16 15 eqcoms
 |-  ( ( # ` F ) = 2 -> ( P ` 2 ) = ( P ` ( # ` F ) ) )
17 16 eqeq1d
 |-  ( ( # ` F ) = 2 -> ( ( P ` 2 ) = C <-> ( P ` ( # ` F ) ) = C ) )
18 17 biimpcd
 |-  ( ( P ` 2 ) = C -> ( ( # ` F ) = 2 -> ( P ` ( # ` F ) ) = C ) )
19 18 eqcoms
 |-  ( C = ( P ` 2 ) -> ( ( # ` F ) = 2 -> ( P ` ( # ` F ) ) = C ) )
20 19 3ad2ant3
 |-  ( ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) -> ( ( # ` F ) = 2 -> ( P ` ( # ` F ) ) = C ) )
21 20 com12
 |-  ( ( # ` F ) = 2 -> ( ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) -> ( P ` ( # ` F ) ) = C ) )
22 21 a1i
 |-  ( F ( Walks ` G ) P -> ( ( # ` F ) = 2 -> ( ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) -> ( P ` ( # ` F ) ) = C ) ) )
23 22 3imp
 |-  ( ( F ( Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) -> ( P ` ( # ` F ) ) = C )
24 10 14 23 3jca
 |-  ( ( F ( Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) -> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = C ) )
25 9 24 syl
 |-  ( ph -> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = C ) )
26 3anass
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) <-> ( G e. UMGraph /\ ( { A , B } e. E /\ { B , C } e. E ) ) )
27 5 6 26 sylanbrc
 |-  ( ph -> ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) )
28 1 umgr2adedgwlklem
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( ( A =/= B /\ B =/= C ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )
29 3simpb
 |-  ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
30 29 adantl
 |-  ( ( ( A =/= B /\ B =/= C ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
31 27 28 30 3syl
 |-  ( ph -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
32 3anass
 |-  ( ( G e. UMGraph /\ A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) <-> ( G e. UMGraph /\ ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )
33 5 31 32 sylanbrc
 |-  ( ph -> ( G e. UMGraph /\ A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
34 s2cli
 |-  <" J K "> e. Word _V
35 3 34 eqeltri
 |-  F e. Word _V
36 s3cli
 |-  <" A B C "> e. Word _V
37 4 36 eqeltri
 |-  P e. Word _V
38 35 37 pm3.2i
 |-  ( F e. Word _V /\ P e. Word _V )
39 id
 |-  ( ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
40 39 3adant1
 |-  ( ( G e. UMGraph /\ A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) -> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
41 40 anim1i
 |-  ( ( ( G e. UMGraph /\ A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) /\ ( F e. Word _V /\ P e. Word _V ) ) -> ( ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) /\ ( F e. Word _V /\ P e. Word _V ) ) )
42 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
43 42 iswlkon
 |-  ( ( ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) /\ ( F e. Word _V /\ P e. Word _V ) ) -> ( F ( A ( WalksOn ` G ) C ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = C ) ) )
44 41 43 syl
 |-  ( ( ( G e. UMGraph /\ A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) /\ ( F e. Word _V /\ P e. Word _V ) ) -> ( F ( A ( WalksOn ` G ) C ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = C ) ) )
45 33 38 44 sylancl
 |-  ( ph -> ( F ( A ( WalksOn ` G ) C ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = C ) ) )
46 25 45 mpbird
 |-  ( ph -> F ( A ( WalksOn ` G ) C ) P )