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 \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ) \land W cyclShift N = U cyclShift M) \to \|W\| = \|U\|$

Proof

Step	Hyp	Ref	Expression
1		cshwlen	$⊢ (W \in Word V \land N \in ℤ) \to \|W cyclShift N\| = \|W\|$
2	1	ad2ant2r	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to \|W cyclShift N\| = \|W\|$
3	2	eqcomd	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to \|W\| = \|W cyclShift N\|$
4	3	3adant3	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ) \land W cyclShift N = U cyclShift M) \to \|W\| = \|W cyclShift N\|$
5		fveq2	$⊢ W cyclShift N = U cyclShift M \to \|W cyclShift N\| = \|U cyclShift M\|$
6	5	3ad2ant3	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ) \land W cyclShift N = U cyclShift M) \to \|W cyclShift N\| = \|U cyclShift M\|$
7		cshwlen	$⊢ (U \in Word V \land M \in ℤ) \to \|U cyclShift M\| = \|U\|$
8	7	ad2ant2l	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to \|U cyclShift M\| = \|U\|$
9	8	3adant3	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ) \land W cyclShift N = U cyclShift M) \to \|U cyclShift M\| = \|U\|$
10	4 6 9	3eqtrd	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ) \land W cyclShift N = U cyclShift M) \to \|W\| = \|U\|$