cshwrnid

Description: Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023)

		Ref	Expression
	Assertion	cshwrnid	$⊢ (W \in Word V \land N \in ℤ) \to ran (W cyclShift N) = ran W$

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	$⊢ i \in (0 ..^\|W\|) \to i \in ℤ$
2	1	3ad2ant3	$⊢ (W \in Word V \land N \in ℤ \land i \in (0 ..^\|W\|)) \to i \in ℤ$
3		simp2	$⊢ (W \in Word V \land N \in ℤ \land i \in (0 ..^\|W\|)) \to N \in ℤ$
4	2 3	zsubcld	$⊢ (W \in Word V \land N \in ℤ \land i \in (0 ..^\|W\|)) \to i - N \in ℤ$
5		elfzo0	$⊢ i \in (0 ..^\|W\|) \leftrightarrow (i \in ℕ_{0} \land \|W\| \in ℕ \land i < \|W\|)$
6	5	simp2bi	$⊢ i \in (0 ..^\|W\|) \to \|W\| \in ℕ$
7	6	3ad2ant3	$⊢ (W \in Word V \land N \in ℤ \land i \in (0 ..^\|W\|)) \to \|W\| \in ℕ$
8		zmodfzo	$⊢ (i - N \in ℤ \land \|W\| \in ℕ) \to (i - N) \mod \|W\| \in (0 ..^\|W\|)$
9	4 7 8	syl2anc	$⊢ (W \in Word V \land N \in ℤ \land i \in (0 ..^\|W\|)) \to (i - N) \mod \|W\| \in (0 ..^\|W\|)$
10	9	3expa	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (i - N) \mod \|W\| \in (0 ..^\|W\|)$
11		elfzoelz	$⊢ j \in (0 ..^\|W\|) \to j \in ℤ$
12	11	adantl	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to j \in ℤ$
13		simplr	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to N \in ℤ$
14	12 13	zaddcld	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to j + N \in ℤ$
15		elfzo0	$⊢ j \in (0 ..^\|W\|) \leftrightarrow (j \in ℕ_{0} \land \|W\| \in ℕ \land j < \|W\|)$
16	15	simp2bi	$⊢ j \in (0 ..^\|W\|) \to \|W\| \in ℕ$
17	16	adantl	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to \|W\| \in ℕ$
18		zmodfzo	$⊢ (j + N \in ℤ \land \|W\| \in ℕ) \to (j + N) \mod \|W\| \in (0 ..^\|W\|)$
19	14 17 18	syl2anc	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to (j + N) \mod \|W\| \in (0 ..^\|W\|)$
20		simpr	$⊢ (((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \land i = (j + N) \mod \|W\|) \to i = (j + N) \mod \|W\|$
21	20	oveq1d	$⊢ (((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \land i = (j + N) \mod \|W\|) \to i - N = ((j + N) \mod \|W\|) - N$
22	21	oveq1d	$⊢ (((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \land i = (j + N) \mod \|W\|) \to (i - N) \mod \|W\| = (((j + N) \mod \|W\|) - N) \mod \|W\|$
23	22	eqeq2d	$⊢ (((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \land i = (j + N) \mod \|W\|) \to (j = (i - N) \mod \|W\| \leftrightarrow j = (((j + N) \mod \|W\|) - N) \mod \|W\|)$
24	12	zred	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to j \in ℝ$
25	13	zred	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to N \in ℝ$
26	24 25	readdcld	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to j + N \in ℝ$
27	17	nnrpd	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to \|W\| \in ℝ^{+}$
28		modsubmod	$⊢ (j + N \in ℝ \land N \in ℝ \land \|W\| \in ℝ^{+}) \to (((j + N) \mod \|W\|) - N) \mod \|W\| = (j + N - N) \mod \|W\|$
29	26 25 27 28	syl3anc	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to (((j + N) \mod \|W\|) - N) \mod \|W\| = (j + N - N) \mod \|W\|$
30	12	zcnd	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to j \in ℂ$
31	13	zcnd	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to N \in ℂ$
32	30 31	pncand	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to j + N - N = j$
33	32	oveq1d	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to (j + N - N) \mod \|W\| = j \mod \|W\|$
34		zmodidfzoimp	$⊢ j \in (0 ..^\|W\|) \to j \mod \|W\| = j$
35	34	adantl	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to j \mod \|W\| = j$
36	29 33 35	3eqtrrd	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to j = (((j + N) \mod \|W\|) - N) \mod \|W\|$
37	19 23 36	rspcedvd	$⊢ ((W \in Word V \land N \in ℤ) \land j \in (0 ..^\|W\|)) \to \exists i \in (0 ..^\|W\|) j = (i - N) \mod \|W\|$
38		simp3	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|) \land j = (i - N) \mod \|W\|) \to j = (i - N) \mod \|W\|$
39	38	fveq2d	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|) \land j = (i - N) \mod \|W\|) \to (W cyclShift N) (j) = (W cyclShift N) ((i - N) \mod \|W\|)$
40		simp1l	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|) \land j = (i - N) \mod \|W\|) \to W \in Word V$
41		simp1r	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|) \land j = (i - N) \mod \|W\|) \to N \in ℤ$
42		simp2	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|) \land j = (i - N) \mod \|W\|) \to i \in (0 ..^\|W\|)$
43		cshwidxmodr	$⊢ (W \in Word V \land N \in ℤ \land i \in (0 ..^\|W\|)) \to (W cyclShift N) ((i - N) \mod \|W\|) = W (i)$
44	40 41 42 43	syl3anc	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|) \land j = (i - N) \mod \|W\|) \to (W cyclShift N) ((i - N) \mod \|W\|) = W (i)$
45	39 44	eqtrd	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|) \land j = (i - N) \mod \|W\|) \to (W cyclShift N) (j) = W (i)$
46	45	eqeq2d	$⊢ ((W \in Word V \land N \in ℤ) \land i \in (0 ..^\|W\|) \land j = (i - N) \mod \|W\|) \to (c = (W cyclShift N) (j) \leftrightarrow c = W (i))$
47	10 37 46	rexxfrd2	$⊢ (W \in Word V \land N \in ℤ) \to (\exists j \in (0 ..^\|W\|) c = (W cyclShift N) (j) \leftrightarrow \exists i \in (0 ..^\|W\|) c = W (i))$
48	47	abbidv	$⊢ (W \in Word V \land N \in ℤ) \to \{c \| \exists j \in (0 ..^\|W\|) c = (W cyclShift N) (j)\} = \{c \| \exists i \in (0 ..^\|W\|) c = W (i)\}$
49		cshwfn	$⊢ (W \in Word V \land N \in ℤ) \to (W cyclShift N) Fn (0 ..^\|W\|)$
50		fnrnfv	$⊢ (W cyclShift N) Fn (0 ..^\|W\|) \to ran (W cyclShift N) = \{c \| \exists j \in (0 ..^\|W\|) c = (W cyclShift N) (j)\}$
51	49 50	syl	$⊢ (W \in Word V \land N \in ℤ) \to ran (W cyclShift N) = \{c \| \exists j \in (0 ..^\|W\|) c = (W cyclShift N) (j)\}$
52		wrdfn	$⊢ W \in Word V \to W Fn (0 ..^\|W\|)$
53	52	adantr	$⊢ (W \in Word V \land N \in ℤ) \to W Fn (0 ..^\|W\|)$
54		fnrnfv	$⊢ W Fn (0 ..^\|W\|) \to ran W = \{c \| \exists i \in (0 ..^\|W\|) c = W (i)\}$
55	53 54	syl	$⊢ (W \in Word V \land N \in ℤ) \to ran W = \{c \| \exists i \in (0 ..^\|W\|) c = W (i)\}$
56	48 51 55	3eqtr4d	$⊢ (W \in Word V \land N \in ℤ) \to ran (W cyclShift N) = ran W$

Metamath Proof Explorer

Theorem cshwrnid

Proof