Metamath Proof Explorer


Theorem 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 ..^ ( ♯ ‘ 𝑊 ) ) )