Metamath Proof Explorer

Theorem cshwleneq

Description: If the results of cyclically shifting two words are equal, the length of the two words was equal. (Contributed by AV, 21-Apr-2018) (Revised by AV, 5-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion cshwleneq 
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( # ` W ) = ( # ` U ) )

Proof

Step Hyp Ref Expression
1 cshwlen 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
2 1 ad2ant2r 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
3 2 eqcomd 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( # ` W ) = ( # ` ( W cyclShift N ) ) )
4 3 3adant3 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( # ` W ) = ( # ` ( W cyclShift N ) ) )
5 fveq2 
 |-  ( ( W cyclShift N ) = ( U cyclShift M ) -> ( # ` ( W cyclShift N ) ) = ( # ` ( U cyclShift M ) ) )
6 5 3ad2ant3 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( # ` ( W cyclShift N ) ) = ( # ` ( U cyclShift M ) ) )
7 cshwlen 
 |-  ( ( U e. Word V /\ M e. ZZ ) -> ( # ` ( U cyclShift M ) ) = ( # ` U ) )
8 7 ad2ant2l 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( # ` ( U cyclShift M ) ) = ( # ` U ) )
9 8 3adant3 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( # ` ( U cyclShift M ) ) = ( # ` U ) )
10 4 6 9 3eqtrd 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( # ` W ) = ( # ` U ) )