Metamath Proof Explorer

Theorem wwlkseq

Description: Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021)

Ref Expression
Assertion wwlkseq 
|- ( ( W e. ( WWalks ` G ) /\ T e. ( WWalks ` G ) ) -> ( W = T <-> ( ( # ` W ) = ( # ` T ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( T ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 wwlkbp 
 |-  ( W e. ( WWalks ` G ) -> ( G e. _V /\ W e. Word ( Vtx ` G ) ) )
3 2 simprd 
 |-  ( W e. ( WWalks ` G ) -> W e. Word ( Vtx ` G ) )
4 1 wwlkbp 
 |-  ( T e. ( WWalks ` G ) -> ( G e. _V /\ T e. Word ( Vtx ` G ) ) )
5 4 simprd 
 |-  ( T e. ( WWalks ` G ) -> T e. Word ( Vtx ` G ) )
6 eqwrd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ T e. Word ( Vtx ` G ) ) -> ( W = T <-> ( ( # ` W ) = ( # ` T ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( T ` i ) ) ) )
7 3 5 6 syl2an 
 |-  ( ( W e. ( WWalks ` G ) /\ T e. ( WWalks ` G ) ) -> ( W = T <-> ( ( # ` W ) = ( # ` T ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( T ` i ) ) ) )