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	$$⊢\left(W\in \mathrm{Word}V\wedge N\in \mathbb{Z}\right)\to \mathrm{ran}\left(W\mathrm{cyclShift}N\right)\subseteq V$$

Proof

Step	Hyp	Ref	Expression
1		cshwf	$$⊢\left(W\in \mathrm{Word}V\wedge N\in \mathbb{Z}\right)\to \left(W\mathrm{cyclShift}N\right):\left(0..^\left|W\right|\right)⟶V$$
2	1	frnd	$$⊢\left(W\in \mathrm{Word}V\wedge N\in \mathbb{Z}\right)\to \mathrm{ran}\left(W\mathrm{cyclShift}N\right)\subseteq V$$