Metamath Proof Explorer

Theorem cshwrn

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 ⊢ W ∈ Word V ∧ N ∈ ℤ → ran ⁡ W cyclShift N ⊆ V

Proof

Step Hyp Ref Expression
1 cshwf ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N : 0 ..^ W ⟶ V
2 1 frnd ⊢ W ∈ Word V ∧ N ∈ ℤ → ran ⁡ W cyclShift N ⊆ V