Metamath Proof Explorer

Theorem cshwidx0mod

Description: The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N (modulo the length of the word) of the original word. (Contributed by AV, 30-Oct-2018)

		Ref	Expression
	Assertion	cshwidx0mod	$⊢ (W \in Word V \land W \neq \emptyset \land N \in ℤ) \to (W cyclShift N) (0) = W (N \mod \|W\|)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (W \in Word V \land W \neq \emptyset \land N \in ℤ) \to W \in Word V$
2		simp3	$⊢ (W \in Word V \land W \neq \emptyset \land N \in ℤ) \to N \in ℤ$
3		lennncl	$⊢ (W \in Word V \land W \neq \emptyset) \to \|W\| \in ℕ$
4		lbfzo0	$⊢ 0 \in (0 ..^\|W\|) \leftrightarrow \|W\| \in ℕ$
5	3 4	sylibr	$⊢ (W \in Word V \land W \neq \emptyset) \to 0 \in (0 ..^\|W\|)$
6	5	3adant3	$⊢ (W \in Word V \land W \neq \emptyset \land N \in ℤ) \to 0 \in (0 ..^\|W\|)$
7		cshwidxmod	$⊢ (W \in Word V \land N \in ℤ \land 0 \in (0 ..^\|W\|)) \to (W cyclShift N) (0) = W ((0 + N) \mod \|W\|)$
8	1 2 6 7	syl3anc	$⊢ (W \in Word V \land W \neq \emptyset \land N \in ℤ) \to (W cyclShift N) (0) = W ((0 + N) \mod \|W\|)$
9		zcn	$⊢ N \in ℤ \to N \in ℂ$
10	9	addid2d	$⊢ N \in ℤ \to 0 + N = N$
11	10	3ad2ant3	$⊢ (W \in Word V \land W \neq \emptyset \land N \in ℤ) \to 0 + N = N$
12	11	fvoveq1d	$⊢ (W \in Word V \land W \neq \emptyset \land N \in ℤ) \to W ((0 + N) \mod \|W\|) = W (N \mod \|W\|)$
13	8 12	eqtrd	$⊢ (W \in Word V \land W \neq \emptyset \land N \in ℤ) \to (W cyclShift N) (0) = W (N \mod \|W\|)$