Metamath Proof Explorer

Theorem cshwcl

Description: A cyclically shifted word is a word over the same set as for the original word. (Contributed by AV, 16-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 27-Oct-2018)

		Ref	Expression
	Assertion	cshwcl	$⊢ W \in Word V \to W cyclShift N \in Word V$

Proof

Step	Hyp	Ref	Expression
1		cshword	$⊢ (W \in Word V \land N \in ℤ) \to W cyclShift N = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
2		swrdcl	$⊢ W \in Word V \to W substr ⟨N \mod \|W\|, \|W\|⟩ \in Word V$
3		pfxcl	$⊢ W \in Word V \to W prefix (N \mod \|W\|) \in Word V$
4		ccatcl	$⊢ (W substr ⟨N \mod \|W\|, \|W\|⟩ \in Word V \land W prefix (N \mod \|W\|) \in Word V) \to (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|)) \in Word V$
5	2 3 4	syl2anc	$⊢ W \in Word V \to (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|)) \in Word V$
6	5	adantr	$⊢ (W \in Word V \land N \in ℤ) \to (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|)) \in Word V$
7	1 6	eqeltrd	$⊢ (W \in Word V \land N \in ℤ) \to W cyclShift N \in Word V$
8	7	expcom	$⊢ N \in ℤ \to (W \in Word V \to W cyclShift N \in Word V)$
9		cshnz	$⊢ \neg N \in ℤ \to W cyclShift N = \emptyset$
10		wrd0	$⊢ \emptyset \in Word V$
11	9 10	eqeltrdi	$⊢ \neg N \in ℤ \to W cyclShift N \in Word V$
12	11	a1d	$⊢ \neg N \in ℤ \to (W \in Word V \to W cyclShift N \in Word V)$
13	8 12	pm2.61i	$⊢ W \in Word V \to W cyclShift N \in Word V$