cshweqrep

Description: If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by AV, 13-May-2018) (Revised by AV, 7-Jun-2018) (Revised by AV, 1-Nov-2018)

		Ref	Expression
	Assertion	cshweqrep	$⊢ (W \in Word V \land L \in ℤ) \to ((W cyclShift L = W \land I \in (0 ..^\|W\|)) \to \forall j \in ℕ_{0} W (I) = W ((I + j L) \mod \|W\|))$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ x = 0 \to x L = 0 \cdot L$
2	1	oveq2d	$⊢ x = 0 \to I + x L = I + 0 \cdot L$
3	2	fvoveq1d	$⊢ x = 0 \to W ((I + x L) \mod \|W\|) = W ((I + 0 \cdot L) \mod \|W\|)$
4	3	eqeq2d	$⊢ x = 0 \to (W (I) = W ((I + x L) \mod \|W\|) \leftrightarrow W (I) = W ((I + 0 \cdot L) \mod \|W\|))$
5	4	imbi2d	$⊢ x = 0 \to ((((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + x L) \mod \|W\|)) \leftrightarrow (((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + 0 \cdot L) \mod \|W\|)))$
6		oveq1	$⊢ x = y \to x L = y L$
7	6	oveq2d	$⊢ x = y \to I + x L = I + y L$
8	7	fvoveq1d	$⊢ x = y \to W ((I + x L) \mod \|W\|) = W ((I + y L) \mod \|W\|)$
9	8	eqeq2d	$⊢ x = y \to (W (I) = W ((I + x L) \mod \|W\|) \leftrightarrow W (I) = W ((I + y L) \mod \|W\|))$
10	9	imbi2d	$⊢ x = y \to ((((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + x L) \mod \|W\|)) \leftrightarrow (((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + y L) \mod \|W\|)))$
11		oveq1	$⊢ x = y + 1 \to x L = (y + 1) L$
12	11	oveq2d	$⊢ x = y + 1 \to I + x L = I + (y + 1) L$
13	12	fvoveq1d	$⊢ x = y + 1 \to W ((I + x L) \mod \|W\|) = W ((I + (y + 1) L) \mod \|W\|)$
14	13	eqeq2d	$⊢ x = y + 1 \to (W (I) = W ((I + x L) \mod \|W\|) \leftrightarrow W (I) = W ((I + (y + 1) L) \mod \|W\|))$
15	14	imbi2d	$⊢ x = y + 1 \to ((((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + x L) \mod \|W\|)) \leftrightarrow (((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + (y + 1) L) \mod \|W\|)))$
16		oveq1	$⊢ x = j \to x L = j L$
17	16	oveq2d	$⊢ x = j \to I + x L = I + j L$
18	17	fvoveq1d	$⊢ x = j \to W ((I + x L) \mod \|W\|) = W ((I + j L) \mod \|W\|)$
19	18	eqeq2d	$⊢ x = j \to (W (I) = W ((I + x L) \mod \|W\|) \leftrightarrow W (I) = W ((I + j L) \mod \|W\|))$
20	19	imbi2d	$⊢ x = j \to ((((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + x L) \mod \|W\|)) \leftrightarrow (((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + j L) \mod \|W\|)))$
21		zcn	$⊢ L \in ℤ \to L \in ℂ$
22	21	mul02d	$⊢ L \in ℤ \to 0 \cdot L = 0$
23	22	adantl	$⊢ (W \in Word V \land L \in ℤ) \to 0 \cdot L = 0$
24	23	adantr	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to 0 \cdot L = 0$
25	24	oveq2d	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to I + 0 \cdot L = I + 0$
26		elfzoelz	$⊢ I \in (0 ..^\|W\|) \to I \in ℤ$
27	26	zcnd	$⊢ I \in (0 ..^\|W\|) \to I \in ℂ$
28	27	addridd	$⊢ I \in (0 ..^\|W\|) \to I + 0 = I$
29	28	ad2antll	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to I + 0 = I$
30	25 29	eqtrd	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to I + 0 \cdot L = I$
31	30	oveq1d	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to (I + 0 \cdot L) \mod \|W\| = I \mod \|W\|$
32		zmodidfzoimp	$⊢ I \in (0 ..^\|W\|) \to I \mod \|W\| = I$
33	32	ad2antll	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to I \mod \|W\| = I$
34	31 33	eqtr2d	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to I = (I + 0 \cdot L) \mod \|W\|$
35	34	fveq2d	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + 0 \cdot L) \mod \|W\|)$
36		fveq1	$⊢ W = W cyclShift L \to W ((I + y L) \mod \|W\|) = (W cyclShift L) ((I + y L) \mod \|W\|)$
37	36	eqcoms	$⊢ W cyclShift L = W \to W ((I + y L) \mod \|W\|) = (W cyclShift L) ((I + y L) \mod \|W\|)$
38	37	ad2antrl	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W ((I + y L) \mod \|W\|) = (W cyclShift L) ((I + y L) \mod \|W\|)$
39	38	adantl	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to W ((I + y L) \mod \|W\|) = (W cyclShift L) ((I + y L) \mod \|W\|)$
40		simprll	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to W \in Word V$
41		simprlr	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to L \in ℤ$
42		elfzo0	$⊢ I \in (0 ..^\|W\|) \leftrightarrow (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|)$
43		nn0z	$⊢ I \in ℕ_{0} \to I \in ℤ$
44	43	adantr	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ) \to I \in ℤ$
45		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
46		zmulcl	$⊢ (y \in ℤ \land L \in ℤ) \to y L \in ℤ$
47	45 46	sylan	$⊢ (y \in ℕ_{0} \land L \in ℤ) \to y L \in ℤ$
48	47	ancoms	$⊢ (L \in ℤ \land y \in ℕ_{0}) \to y L \in ℤ$
49		zaddcl	$⊢ (I \in ℤ \land y L \in ℤ) \to I + y L \in ℤ$
50	44 48 49	syl2an	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ) \land (L \in ℤ \land y \in ℕ_{0})) \to I + y L \in ℤ$
51		simplr	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ) \land (L \in ℤ \land y \in ℕ_{0})) \to \|W\| \in ℕ$
52	50 51	jca	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ) \land (L \in ℤ \land y \in ℕ_{0})) \to (I + y L \in ℤ \land \|W\| \in ℕ)$
53	52	ex	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ) \to ((L \in ℤ \land y \in ℕ_{0}) \to (I + y L \in ℤ \land \|W\| \in ℕ))$
54	53	3adant3	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|) \to ((L \in ℤ \land y \in ℕ_{0}) \to (I + y L \in ℤ \land \|W\| \in ℕ))$
55	42 54	sylbi	$⊢ I \in (0 ..^\|W\|) \to ((L \in ℤ \land y \in ℕ_{0}) \to (I + y L \in ℤ \land \|W\| \in ℕ))$
56	55	adantl	$⊢ (W cyclShift L = W \land I \in (0 ..^\|W\|)) \to ((L \in ℤ \land y \in ℕ_{0}) \to (I + y L \in ℤ \land \|W\| \in ℕ))$
57	56	expd	$⊢ (W cyclShift L = W \land I \in (0 ..^\|W\|)) \to (L \in ℤ \to (y \in ℕ_{0} \to (I + y L \in ℤ \land \|W\| \in ℕ)))$
58	57	com12	$⊢ L \in ℤ \to ((W cyclShift L = W \land I \in (0 ..^\|W\|)) \to (y \in ℕ_{0} \to (I + y L \in ℤ \land \|W\| \in ℕ)))$
59	58	adantl	$⊢ (W \in Word V \land L \in ℤ) \to ((W cyclShift L = W \land I \in (0 ..^\|W\|)) \to (y \in ℕ_{0} \to (I + y L \in ℤ \land \|W\| \in ℕ)))$
60	59	imp	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to (y \in ℕ_{0} \to (I + y L \in ℤ \land \|W\| \in ℕ))$
61	60	impcom	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to (I + y L \in ℤ \land \|W\| \in ℕ)$
62		zmodfzo	$⊢ (I + y L \in ℤ \land \|W\| \in ℕ) \to (I + y L) \mod \|W\| \in (0 ..^\|W\|)$
63	61 62	syl	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to (I + y L) \mod \|W\| \in (0 ..^\|W\|)$
64		cshwidxmod	$⊢ (W \in Word V \land L \in ℤ \land (I + y L) \mod \|W\| \in (0 ..^\|W\|)) \to (W cyclShift L) ((I + y L) \mod \|W\|) = W ((((I + y L) \mod \|W\|) + L) \mod \|W\|)$
65	40 41 63 64	syl3anc	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to (W cyclShift L) ((I + y L) \mod \|W\|) = W ((((I + y L) \mod \|W\|) + L) \mod \|W\|)$
66		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
67		zre	$⊢ L \in ℤ \to L \in ℝ$
68		nn0re	$⊢ y \in ℕ_{0} \to y \in ℝ$
69		nnrp	$⊢ \|W\| \in ℕ \to \|W\| \in ℝ^{+}$
70		remulcl	$⊢ (y \in ℝ \land L \in ℝ) \to y L \in ℝ$
71	70	ancoms	$⊢ (L \in ℝ \land y \in ℝ) \to y L \in ℝ$
72		readdcl	$⊢ (I \in ℝ \land y L \in ℝ) \to I + y L \in ℝ$
73	71 72	sylan2	$⊢ (I \in ℝ \land (L \in ℝ \land y \in ℝ)) \to I + y L \in ℝ$
74	73	ancoms	$⊢ ((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to I + y L \in ℝ$
75	74	adantl	$⊢ (\|W\| \in ℝ^{+} \land ((L \in ℝ \land y \in ℝ) \land I \in ℝ)) \to I + y L \in ℝ$
76		simprll	$⊢ (\|W\| \in ℝ^{+} \land ((L \in ℝ \land y \in ℝ) \land I \in ℝ)) \to L \in ℝ$
77		simpl	$⊢ (\|W\| \in ℝ^{+} \land ((L \in ℝ \land y \in ℝ) \land I \in ℝ)) \to \|W\| \in ℝ^{+}$
78		modaddmod	$⊢ (I + y L \in ℝ \land L \in ℝ \land \|W\| \in ℝ^{+}) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + y L + L) \mod \|W\|$
79	75 76 77 78	syl3anc	$⊢ (\|W\| \in ℝ^{+} \land ((L \in ℝ \land y \in ℝ) \land I \in ℝ)) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + y L + L) \mod \|W\|$
80		recn	$⊢ I \in ℝ \to I \in ℂ$
81	80	adantl	$⊢ ((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to I \in ℂ$
82	70	recnd	$⊢ (y \in ℝ \land L \in ℝ) \to y L \in ℂ$
83	82	ancoms	$⊢ (L \in ℝ \land y \in ℝ) \to y L \in ℂ$
84	83	adantr	$⊢ ((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to y L \in ℂ$
85		recn	$⊢ L \in ℝ \to L \in ℂ$
86	85	adantr	$⊢ (L \in ℝ \land y \in ℝ) \to L \in ℂ$
87	86	adantr	$⊢ ((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to L \in ℂ$
88	81 84 87	addassd	$⊢ ((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to I + y L + L = I + y L + L$
89		recn	$⊢ y \in ℝ \to y \in ℂ$
90	89	adantl	$⊢ (L \in ℝ \land y \in ℝ) \to y \in ℂ$
91		1cnd	$⊢ (L \in ℝ \land y \in ℝ) \to 1 \in ℂ$
92	90 91 86	adddird	$⊢ (L \in ℝ \land y \in ℝ) \to (y + 1) L = y L + 1 L$
93	85	mullidd	$⊢ L \in ℝ \to 1 L = L$
94	93	adantr	$⊢ (L \in ℝ \land y \in ℝ) \to 1 L = L$
95	94	oveq2d	$⊢ (L \in ℝ \land y \in ℝ) \to y L + 1 L = y L + L$
96	92 95	eqtr2d	$⊢ (L \in ℝ \land y \in ℝ) \to y L + L = (y + 1) L$
97	96	adantr	$⊢ ((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to y L + L = (y + 1) L$
98	97	oveq2d	$⊢ ((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to I + y L + L = I + (y + 1) L$
99	88 98	eqtrd	$⊢ ((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to I + y L + L = I + (y + 1) L$
100	99	adantl	$⊢ (\|W\| \in ℝ^{+} \land ((L \in ℝ \land y \in ℝ) \land I \in ℝ)) \to I + y L + L = I + (y + 1) L$
101	100	oveq1d	$⊢ (\|W\| \in ℝ^{+} \land ((L \in ℝ \land y \in ℝ) \land I \in ℝ)) \to (I + y L + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|$
102	79 101	eqtrd	$⊢ (\|W\| \in ℝ^{+} \land ((L \in ℝ \land y \in ℝ) \land I \in ℝ)) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|$
103	102	ex	$⊢ \|W\| \in ℝ^{+} \to (((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|)$
104	69 103	syl	$⊢ \|W\| \in ℕ \to (((L \in ℝ \land y \in ℝ) \land I \in ℝ) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|)$
105	104	expd	$⊢ \|W\| \in ℕ \to ((L \in ℝ \land y \in ℝ) \to (I \in ℝ \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|))$
106	105	com12	$⊢ (L \in ℝ \land y \in ℝ) \to (\|W\| \in ℕ \to (I \in ℝ \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|))$
107	67 68 106	syl2an	$⊢ (L \in ℤ \land y \in ℕ_{0}) \to (\|W\| \in ℕ \to (I \in ℝ \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|))$
108	107	com13	$⊢ I \in ℝ \to (\|W\| \in ℕ \to ((L \in ℤ \land y \in ℕ_{0}) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|))$
109	66 108	syl	$⊢ I \in ℕ_{0} \to (\|W\| \in ℕ \to ((L \in ℤ \land y \in ℕ_{0}) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|))$
110	109	imp	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ) \to ((L \in ℤ \land y \in ℕ_{0}) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|)$
111	110	3adant3	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|) \to ((L \in ℤ \land y \in ℕ_{0}) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|)$
112	42 111	sylbi	$⊢ I \in (0 ..^\|W\|) \to ((L \in ℤ \land y \in ℕ_{0}) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|)$
113	112	expd	$⊢ I \in (0 ..^\|W\|) \to (L \in ℤ \to (y \in ℕ_{0} \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|))$
114	113	adantld	$⊢ I \in (0 ..^\|W\|) \to ((W \in Word V \land L \in ℤ) \to (y \in ℕ_{0} \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|))$
115	114	adantl	$⊢ (W cyclShift L = W \land I \in (0 ..^\|W\|)) \to ((W \in Word V \land L \in ℤ) \to (y \in ℕ_{0} \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|))$
116	115	impcom	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to (y \in ℕ_{0} \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|)$
117	116	impcom	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to (((I + y L) \mod \|W\|) + L) \mod \|W\| = (I + (y + 1) L) \mod \|W\|$
118	117	fveq2d	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to W ((((I + y L) \mod \|W\|) + L) \mod \|W\|) = W ((I + (y + 1) L) \mod \|W\|)$
119	39 65 118	3eqtrd	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to W ((I + y L) \mod \|W\|) = W ((I + (y + 1) L) \mod \|W\|)$
120	119	eqeq2d	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to (W (I) = W ((I + y L) \mod \|W\|) \leftrightarrow W (I) = W ((I + (y + 1) L) \mod \|W\|))$
121	120	biimpd	$⊢ (y \in ℕ_{0} \land ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|)))) \to (W (I) = W ((I + y L) \mod \|W\|) \to W (I) = W ((I + (y + 1) L) \mod \|W\|))$
122	121	ex	$⊢ y \in ℕ_{0} \to (((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to (W (I) = W ((I + y L) \mod \|W\|) \to W (I) = W ((I + (y + 1) L) \mod \|W\|)))$
123	122	a2d	$⊢ y \in ℕ_{0} \to ((((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + y L) \mod \|W\|)) \to (((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + (y + 1) L) \mod \|W\|)))$
124	5 10 15 20 35 123	nn0ind	$⊢ j \in ℕ_{0} \to (((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to W (I) = W ((I + j L) \mod \|W\|))$
125	124	com12	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to (j \in ℕ_{0} \to W (I) = W ((I + j L) \mod \|W\|))$
126	125	ralrimiv	$⊢ ((W \in Word V \land L \in ℤ) \land (W cyclShift L = W \land I \in (0 ..^\|W\|))) \to \forall j \in ℕ_{0} W (I) = W ((I + j L) \mod \|W\|)$
127	126	ex	$⊢ (W \in Word V \land L \in ℤ) \to ((W cyclShift L = W \land I \in (0 ..^\|W\|)) \to \forall j \in ℕ_{0} W (I) = W ((I + j L) \mod \|W\|))$

Metamath Proof Explorer

Theorem cshweqrep

Proof