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

Metamath Proof Explorer

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