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 )