Theorem erclwwlkneqlen

Description: If two classes are equivalent regarding .~ , then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-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	erclwwlkneqlen	|- ( ( T e. X /\ U e. Y ) -> ( T .~ U -> ( # ` T ) = ( # ` U ) ) )

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	1 2	erclwwlkneq	|- ( ( T e. X /\ U e. Y ) -> ( T .~ U <-> ( T e. W /\ U e. W /\ E. n e. ( 0 ... N ) T = ( U cyclShift n ) ) ) )
4		fveq2	|- ( T = ( U cyclShift n ) -> ( # ` T ) = ( # ` ( U cyclShift n ) ) )
5		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
6	5	clwwlknwrd	|- ( U e. ( N ClWWalksN G ) -> U e. Word ( Vtx ` G ) )
7	6 1	eleq2s	|- ( U e. W -> U e. Word ( Vtx ` G ) )
8	7	adantl	|- ( ( T e. W /\ U e. W ) -> U e. Word ( Vtx ` G ) )
9		elfzelz	|- ( n e. ( 0 ... N ) -> n e. ZZ )
10		cshwlen	|- ( ( U e. Word ( Vtx ` G ) /\ n e. ZZ ) -> ( # ` ( U cyclShift n ) ) = ( # ` U ) )
11	8 9 10	syl2an	|- ( ( ( T e. W /\ U e. W ) /\ n e. ( 0 ... N ) ) -> ( # ` ( U cyclShift n ) ) = ( # ` U ) )
12	4 11	sylan9eqr	|- ( ( ( ( T e. W /\ U e. W ) /\ n e. ( 0 ... N ) ) /\ T = ( U cyclShift n ) ) -> ( # ` T ) = ( # ` U ) )
13	12	rexlimdva2	|- ( ( T e. W /\ U e. W ) -> ( E. n e. ( 0 ... N ) T = ( U cyclShift n ) -> ( # ` T ) = ( # ` U ) ) )
14	13	3impia	|- ( ( T e. W /\ U e. W /\ E. n e. ( 0 ... N ) T = ( U cyclShift n ) ) -> ( # ` T ) = ( # ` U ) )
15	3 14	biimtrdi	|- ( ( T e. X /\ U e. Y ) -> ( T .~ U -> ( # ` T ) = ( # ` U ) ) )