cshwmodn

Description: Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018) (Proof shortened by AV, 16-Oct-2022)

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

Proof

Step	Hyp	Ref	Expression
1		0csh0	$⊢ \emptyset cyclShift N = \emptyset$
2		oveq1	$⊢ W = \emptyset \to W cyclShift N = \emptyset cyclShift N$
3		oveq1	$⊢ W = \emptyset \to W cyclShift (N \mod \|W\|) = \emptyset cyclShift (N \mod \|W\|)$
4		0csh0	$⊢ \emptyset cyclShift (N \mod \|W\|) = \emptyset$
5	3 4	eqtrdi	$⊢ W = \emptyset \to W cyclShift (N \mod \|W\|) = \emptyset$
6	1 2 5	3eqtr4a	$⊢ W = \emptyset \to W cyclShift N = W cyclShift (N \mod \|W\|)$
7	6	a1d	$⊢ W = \emptyset \to ((W \in Word V \land N \in ℤ) \to W cyclShift N = W cyclShift (N \mod \|W\|))$
8		lennncl	$⊢ (W \in Word V \land W \neq \emptyset) \to \|W\| \in ℕ$
9	8	ex	$⊢ W \in Word V \to (W \neq \emptyset \to \|W\| \in ℕ)$
10	9	adantr	$⊢ (W \in Word V \land N \in ℤ) \to (W \neq \emptyset \to \|W\| \in ℕ)$
11	10	impcom	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to \|W\| \in ℕ$
12		simprr	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to N \in ℤ$
13		zre	$⊢ N \in ℤ \to N \in ℝ$
14		nnrp	$⊢ \|W\| \in ℕ \to \|W\| \in ℝ^{+}$
15		modabs2	$⊢ (N \in ℝ \land \|W\| \in ℝ^{+}) \to (N \mod \|W\|) \mod \|W\| = N \mod \|W\|$
16	13 14 15	syl2anr	$⊢ (\|W\| \in ℕ \land N \in ℤ) \to (N \mod \|W\|) \mod \|W\| = N \mod \|W\|$
17	16	opeq1d	$⊢ (\|W\| \in ℕ \land N \in ℤ) \to ⟨(N \mod \|W\|) \mod \|W\|, \|W\|⟩ = ⟨N \mod \|W\|, \|W\|⟩$
18	17	oveq2d	$⊢ (\|W\| \in ℕ \land N \in ℤ) \to W substr ⟨(N \mod \|W\|) \mod \|W\|, \|W\|⟩ = W substr ⟨N \mod \|W\|, \|W\|⟩$
19	16	oveq2d	$⊢ (\|W\| \in ℕ \land N \in ℤ) \to W prefix ((N \mod \|W\|) \mod \|W\|) = W prefix (N \mod \|W\|)$
20	18 19	oveq12d	$⊢ (\|W\| \in ℕ \land N \in ℤ) \to (W substr ⟨(N \mod \|W\|) \mod \|W\|, \|W\|⟩) ++ (W prefix ((N \mod \|W\|) \mod \|W\|)) = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
21	11 12 20	syl2anc	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to (W substr ⟨(N \mod \|W\|) \mod \|W\|, \|W\|⟩) ++ (W prefix ((N \mod \|W\|) \mod \|W\|)) = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
22		simprl	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to W \in Word V$
23	12 11	zmodcld	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to N \mod \|W\| \in ℕ_{0}$
24	23	nn0zd	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to N \mod \|W\| \in ℤ$
25		cshword	$⊢ (W \in Word V \land N \mod \|W\| \in ℤ) \to W cyclShift (N \mod \|W\|) = (W substr ⟨(N \mod \|W\|) \mod \|W\|, \|W\|⟩) ++ (W prefix ((N \mod \|W\|) \mod \|W\|))$
26	22 24 25	syl2anc	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to W cyclShift (N \mod \|W\|) = (W substr ⟨(N \mod \|W\|) \mod \|W\|, \|W\|⟩) ++ (W prefix ((N \mod \|W\|) \mod \|W\|))$
27		cshword	$⊢ (W \in Word V \land N \in ℤ) \to W cyclShift N = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
28	27	adantl	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to W cyclShift N = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
29	21 26 28	3eqtr4rd	$⊢ (W \neq \emptyset \land (W \in Word V \land N \in ℤ)) \to W cyclShift N = W cyclShift (N \mod \|W\|)$
30	29	ex	$⊢ W \neq \emptyset \to ((W \in Word V \land N \in ℤ) \to W cyclShift N = W cyclShift (N \mod \|W\|))$
31	7 30	pm2.61ine	$⊢ (W \in Word V \land N \in ℤ) \to W cyclShift N = W cyclShift (N \mod \|W\|)$

Metamath Proof Explorer

Theorem cshwmodn

Proof