cshweqrep - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cshweqrep		Structured version Visualization version GIF version

Theorem cshweqrep 13418

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.)

**Assertion**
Ref	Expression
cshweqrep	⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ∀𝑗 ∈ ℕ₀ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))

Distinct variable groups: 𝑗,𝐼 𝑗,𝐿 𝑗,𝑉 𝑗,𝑊

Proof of Theorem cshweqrep Dummy variables 𝑦 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (𝑥 · 𝐿) = (0 · 𝐿))
2	1	oveq2d 6565	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (0 · 𝐿)))
3	2	oveq1d 6564	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))
4	3	fveq2d 6107	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))
5	4	eqeq2d 2620	. . . . . 6 ⊢ (𝑥 = 0 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))))
6	5	imbi2d 329	. . . . 5 ⊢ (𝑥 = 0 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))))
7		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥 · 𝐿) = (𝑦 · 𝐿))
8	7	oveq2d 6565	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑦 · 𝐿)))
9	8	oveq1d 6564	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))
10	9	fveq2d 6107	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
11	10	eqeq2d 2620	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))))
12	11	imbi2d 329	. . . . 5 ⊢ (𝑥 = 𝑦 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))))
13		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝐿) = ((𝑦 + 1) · 𝐿))
14	13	oveq2d 6565	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 + 1) → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿)))
15	14	oveq1d 6564	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
16	15	fveq2d 6107	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
17	16	eqeq2d 2620	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
18	17	imbi2d 329	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
19		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → (𝑥 · 𝐿) = (𝑗 · 𝐿))
20	19	oveq2d 6565	. . . . . . . . 9 ⊢ (𝑥 = 𝑗 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑗 · 𝐿)))
21	20	oveq1d 6564	. . . . . . . 8 ⊢ (𝑥 = 𝑗 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))
22	21	fveq2d 6107	. . . . . . 7 ⊢ (𝑥 = 𝑗 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))
23	22	eqeq2d 2620	. . . . . 6 ⊢ (𝑥 = 𝑗 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
24	23	imbi2d 329	. . . . 5 ⊢ (𝑥 = 𝑗 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))))
25		zcn 11259	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ ℤ → 𝐿 ∈ ℂ)
26	25	mul02d 10113	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ ℤ → (0 · 𝐿) = 0)
27	26	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (0 · 𝐿) = 0)
28	27	adantr 480	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (0 · 𝐿) = 0)
29	28	oveq2d 6565	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + (0 · 𝐿)) = (𝐼 + 0))
30		elfzoelz 12339	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℤ)
31	30	zcnd 11359	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℂ)
32	31	addid1d 10115	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 + 0) = 𝐼)
33	32	ad2antll 761	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + 0) = 𝐼)
34	29, 33	eqtrd 2644	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + (0 · 𝐿)) = 𝐼)
35	34	oveq1d 6564	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)) = (𝐼 mod (#‘𝑊)))
36		zmodidfzoimp 12562	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 mod (#‘𝑊)) = 𝐼)
37	36	ad2antll 761	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 mod (#‘𝑊)) = 𝐼)
38	35, 37	eqtr2d 2645	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → 𝐼 = ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))
39	38	fveq2d 6107	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))
40		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑊 = (𝑊 cyclShift 𝐿) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
41	40	eqcoms 2618	. . . . . . . . . . . 12 ⊢ ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
42	41	ad2antrl 760	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
43	42	adantl 481	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
44		simprll 798	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → 𝑊 ∈ Word 𝑉)
45		simprlr 799	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → 𝐿 ∈ ℤ)
46		elfzo0 12376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) ↔ (𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)))
47		nn0z 11277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐼 ∈ ℕ₀ → 𝐼 ∈ ℤ)
48	47	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) → 𝐼 ∈ ℤ)
49		nn0z 11277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ ℤ)
50		zmulcl 11303	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ)
51	49, 50	sylan 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℕ₀ ∧ 𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ)
52	51	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → (𝑦 · 𝐿) ∈ ℤ)
53		zaddcl 11294	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ ℤ ∧ (𝑦 · 𝐿) ∈ ℤ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ)
54	48, 52, 53	syl2an 493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ)
55		simplr 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀)) → (#‘𝑊) ∈ ℕ)
56	54, 55	jca 553	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀)) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
57	56	ex 449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
58	57	3adant3 1074	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
59	46, 58	sylbi 206	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
60	59	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
61	60	expd 451	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ₀ → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
62	61	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ ℤ → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑦 ∈ ℕ₀ → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
63	62	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑦 ∈ ℕ₀ → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
64	63	imp 444	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑦 ∈ ℕ₀ → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
65	64	impcom 445	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
66		zmodfzo 12555	. . . . . . . . . . . 12 ⊢ (((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))
67	65, 66	syl 17	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))
68		cshwidxmod 13400	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ ∧ ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))))
69	44, 45, 67, 68	syl3anc 1318	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))))
70		nn0re 11178	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℕ₀ → 𝐼 ∈ ℝ)
71		zre 11258	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
72		nn0re 11178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ ℝ)
73		nnrp 11718	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑊) ∈ ℕ → (#‘𝑊) ∈ ℝ⁺)
74		remulcl 9900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ)
75	74	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ)
76		readdcl 9898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 ∈ ℝ ∧ (𝑦 · 𝐿) ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
77	75, 76	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐼 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
78	77	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
79	78	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
80		simprll 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → 𝐿 ∈ ℝ)
81		simpl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (#‘𝑊) ∈ ℝ⁺)
82		modaddmod 12571	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐼 + (𝑦 · 𝐿)) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ⁺) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)))
83	79, 80, 81, 82	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)))
84		recn 9905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐼 ∈ ℝ → 𝐼 ∈ ℂ)
85	84	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐼 ∈ ℂ)
86	74	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
87	86	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
88	87	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
89		recn 9905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐿 ∈ ℝ → 𝐿 ∈ ℂ)
90	89	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝐿 ∈ ℂ)
91	90	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐿 ∈ ℂ)
92	85, 88, 91	addassd 9941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 · 𝐿) + 𝐿)))
93		recn 9905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
94	93	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
95		1cnd 9935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
96	94, 95, 90	adddird 9944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 + 1) · 𝐿) = ((𝑦 · 𝐿) + (1 · 𝐿)))
97	89	mulid2d 9937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐿 ∈ ℝ → (1 · 𝐿) = 𝐿)
98	97	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (1 · 𝐿) = 𝐿)
99	98	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + (1 · 𝐿)) = ((𝑦 · 𝐿) + 𝐿))
100	96, 99	eqtr2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿))
101	100	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿))
102	101	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + ((𝑦 · 𝐿) + 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿)))
103	92, 102	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿)))
104	103	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿)))
105	104	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
106	83, 105	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
107	106	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑊) ∈ ℝ⁺ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
108	73, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((#‘𝑊) ∈ ℕ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
109	108	expd 451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
110	109	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
111	71, 72, 110	syl2an 493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
112	111	com13 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℝ → ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
113	70, 112	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ ℕ₀ → ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
114	113	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
115	114	3adant3 1074	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
116	46, 115	sylbi 206	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
117	116	expd 451	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ₀ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
118	117	adantld 482	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (𝑦 ∈ ℕ₀ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
119	118	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (𝑦 ∈ ℕ₀ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
120	119	impcom 445	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑦 ∈ ℕ₀ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
121	120	impcom 445	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
122	121	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
123	43, 69, 122	3eqtrd 2648	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
124	123	eqeq2d 2620	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
125	124	biimpd 218	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
126	125	ex 449	. . . . . 6 ⊢ (𝑦 ∈ ℕ₀ → (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
127	126	a2d 29	. . . . 5 ⊢ (𝑦 ∈ ℕ₀ → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))) → (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
128	6, 12, 18, 24, 39, 127	nn0ind 11348	. . . 4 ⊢ (𝑗 ∈ ℕ₀ → (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
129	128	com12 32	. . 3 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑗 ∈ ℕ₀ → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
130	129	ralrimiv 2948	. 2 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → ∀𝑗 ∈ ℕ₀ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))
131	130	ex 449	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ∀𝑗 ∈ ℕ₀ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 < clt 9953 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ℝ⁺crp 11708 ..^cfzo 12334 mod cmo 12530 #chash 12979 Word cword 13146 cyclShift ccsh 13385

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-fl 12455 df-mod 12531 df-hash 12980 df-word 13154 df-concat 13156 df-substr 13158 df-csh 13386

This theorem is referenced by: cshw1 13419 cshwsidrepsw 15638

W3C validator