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 ) ) ) )