Metamath Proof Explorer


Theorem erclwwlkeq

Description: Two classes are equivalent regarding .~ if both are words and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 29-Apr-2021)

Ref Expression
Hypothesis erclwwlk.r
|- .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
Assertion erclwwlkeq
|- ( ( U e. X /\ W e. Y ) -> ( U .~ W <-> ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) ) )

Proof

Step Hyp Ref Expression
1 erclwwlk.r
 |-  .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
2 eleq1
 |-  ( u = U -> ( u e. ( ClWWalks ` G ) <-> U e. ( ClWWalks ` G ) ) )
3 2 adantr
 |-  ( ( u = U /\ w = W ) -> ( u e. ( ClWWalks ` G ) <-> U e. ( ClWWalks ` G ) ) )
4 eleq1
 |-  ( w = W -> ( w e. ( ClWWalks ` G ) <-> W e. ( ClWWalks ` G ) ) )
5 4 adantl
 |-  ( ( u = U /\ w = W ) -> ( w e. ( ClWWalks ` G ) <-> W e. ( ClWWalks ` G ) ) )
6 fveq2
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
7 6 oveq2d
 |-  ( w = W -> ( 0 ... ( # ` w ) ) = ( 0 ... ( # ` W ) ) )
8 7 adantl
 |-  ( ( u = U /\ w = W ) -> ( 0 ... ( # ` w ) ) = ( 0 ... ( # ` W ) ) )
9 simpl
 |-  ( ( u = U /\ w = W ) -> u = U )
10 oveq1
 |-  ( w = W -> ( w cyclShift n ) = ( W cyclShift n ) )
11 10 adantl
 |-  ( ( u = U /\ w = W ) -> ( w cyclShift n ) = ( W cyclShift n ) )
12 9 11 eqeq12d
 |-  ( ( u = U /\ w = W ) -> ( u = ( w cyclShift n ) <-> U = ( W cyclShift n ) ) )
13 8 12 rexeqbidv
 |-  ( ( u = U /\ w = W ) -> ( E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) <-> E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) )
14 3 5 13 3anbi123d
 |-  ( ( u = U /\ w = W ) -> ( ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) <-> ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) ) )
15 14 1 brabga
 |-  ( ( U e. X /\ W e. Y ) -> ( U .~ W <-> ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) ) )