This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erclwwlkneq

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

Ref Expression
Hypotheses erclwwlkn.w 
|- W = ( N ClWWalksN G )
erclwwlkn.r 
|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion erclwwlkneq 
|- ( ( T e. X /\ U e. Y ) -> ( T .~ U <-> ( T e. W /\ U e. W /\ E. n e. ( 0 ... N ) T = ( U cyclShift n ) ) ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w 
 |-  W = ( N ClWWalksN G )
2 erclwwlkn.r 
 |-  .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3 eleq1 
 |-  ( t = T -> ( t e. W <-> T e. W ) )
4 3 adantr 
 |-  ( ( t = T /\ u = U ) -> ( t e. W <-> T e. W ) )
5 eleq1 
 |-  ( u = U -> ( u e. W <-> U e. W ) )
6 5 adantl 
 |-  ( ( t = T /\ u = U ) -> ( u e. W <-> U e. W ) )
7 simpl 
 |-  ( ( t = T /\ u = U ) -> t = T )
8 oveq1 
 |-  ( u = U -> ( u cyclShift n ) = ( U cyclShift n ) )
9 8 adantl 
 |-  ( ( t = T /\ u = U ) -> ( u cyclShift n ) = ( U cyclShift n ) )
10 7 9 eqeq12d 
 |-  ( ( t = T /\ u = U ) -> ( t = ( u cyclShift n ) <-> T = ( U cyclShift n ) ) )
11 10 rexbidv 
 |-  ( ( t = T /\ u = U ) -> ( E. n e. ( 0 ... N ) t = ( u cyclShift n ) <-> E. n e. ( 0 ... N ) T = ( U cyclShift n ) ) )
12 4 6 11 3anbi123d 
 |-  ( ( t = T /\ u = U ) -> ( ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) <-> ( T e. W /\ U e. W /\ E. n e. ( 0 ... N ) T = ( U cyclShift n ) ) ) )
13 12 2 brabga 
 |-  ( ( T e. X /\ U e. Y ) -> ( T .~ U <-> ( T e. W /\ U e. W /\ E. n e. ( 0 ... N ) T = ( U cyclShift n ) ) ) )