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

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 ( ( ( 𝑊 ∈ 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 𝑀 ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )