This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: The range of a cyclically shifted word is a subset of the set of symbols
for the word. (Contributed by AV, 12-Nov-2018)
|
|
Ref |
Expression |
|
Assertion |
cshwrn |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) ⊆ 𝑉 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cshwf |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 ) |
| 2 |
1
|
frnd |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) ⊆ 𝑉 ) |