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

Metamath Proof Explorer

Theorem cshwf

Description: A cyclically shifted word is a function from a half-open range of integers of the same length as the word as domain to the set of symbols for the word. (Contributed by AV, 12-Nov-2018)

Ref Expression
Assertion cshwf ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )

Proof

Step Hyp Ref Expression
1 cshwcl ⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝐴 )
2 wrdf ⊢ ( ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝐴 → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) ⟶ 𝐴 )
3 1 2 syl ⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) ⟶ 𝐴 )
4 3 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) ⟶ 𝐴 )
5 cshwlen ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
6 5 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 6 feq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) ⟶ 𝐴 ↔ ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ) )
8 4 7 mpbid ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )