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 ∈ Word V ∧ U ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ W cyclShift N = U cyclShift M → W = U

Proof

Step Hyp Ref Expression
1 cshwlen ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W
2 1 ad2ant2r ⊢ W ∈ Word V ∧ U ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N = W
3 2 eqcomd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W = W cyclShift N
4 3 3adant3 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ 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 ∈ Word V ∧ U ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ W cyclShift N = U cyclShift M → W cyclShift N = U cyclShift M
7 cshwlen ⊢ U ∈ Word V ∧ M ∈ ℤ → U cyclShift M = U
8 7 ad2ant2l ⊢ W ∈ Word V ∧ U ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → U cyclShift M = U
9 8 3adant3 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ W cyclShift N = U cyclShift M → U cyclShift M = U
10 4 6 9 3eqtrd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ W cyclShift N = U cyclShift M → W = U