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 W u W n 0 N t = u cyclShift n
Assertion erclwwlkneq T X U Y T ˙ U T W U W n 0 N T = U cyclShift n

Proof

Step Hyp Ref Expression
1 erclwwlkn.w W = N ClWWalksN G
2 erclwwlkn.r ˙ = t u | t W u W n 0 N t = u cyclShift n
3 eleq1 t = T t W T W
4 3 adantr t = T u = U t W T W
5 eleq1 u = U u W U W
6 5 adantl t = T u = U u W U 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 n 0 N t = u cyclShift n n 0 N T = U cyclShift n
12 4 6 11 3anbi123d t = T u = U t W u W n 0 N t = u cyclShift n T W U W n 0 N T = U cyclShift n
13 12 2 brabga T X U Y T ˙ U T W U W n 0 N T = U cyclShift n