This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Words over a set Cyclical shifts of words cshwfn
Description: A cyclically shifted word is a function with a half-open range of integers
of the same length as the word as domain. (Contributed by AV , 12-Nov-2018)
Ref
Expression
Assertion
cshwfn ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
Proof
Step
Hyp
Ref
Expression
1
cshwf ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
2
1
ffnd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )