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