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	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		cshwlen	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
2	1	ad2ant2r	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
3	2	eqcomd	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) )
4	3	3adant3	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) )
5		fveq2	⊢ ( ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑈 cyclShift 𝑀 ) ) )
6	5	3ad2ant3	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑈 cyclShift 𝑀 ) ) )
7		cshwlen	⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ) → ( ♯ ‘ ( 𝑈 cyclShift 𝑀 ) ) = ( ♯ ‘ 𝑈 ) )
8	7	ad2ant2l	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ♯ ‘ ( 𝑈 cyclShift 𝑀 ) ) = ( ♯ ‘ 𝑈 ) )
9	8	3adant3	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ♯ ‘ ( 𝑈 cyclShift 𝑀 ) ) = ( ♯ ‘ 𝑈 ) )
10	4 6 9	3eqtrd	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )