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 13567

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 6657	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (𝑥 · 𝐿) = (0 · 𝐿))
2	1	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (0 · 𝐿)))
3	2	oveq1d 6665	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))
4	3	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))
5	4	eqeq2d 2632	. . . . . 6 ⊢ (𝑥 = 0 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))))
6	5	imbi2d 330	. . . . 5 ⊢ (𝑥 = 0 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))))
7		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥 · 𝐿) = (𝑦 · 𝐿))
8	7	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑦 · 𝐿)))
9	8	oveq1d 6665	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))
10	9	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
11	10	eqeq2d 2632	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))))
12	11	imbi2d 330	. . . . 5 ⊢ (𝑥 = 𝑦 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))))
13		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝐿) = ((𝑦 + 1) · 𝐿))
14	13	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 + 1) → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿)))
15	14	oveq1d 6665	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
16	15	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
17	16	eqeq2d 2632	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
18	17	imbi2d 330	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
19		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → (𝑥 · 𝐿) = (𝑗 · 𝐿))
20	19	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = 𝑗 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑗 · 𝐿)))
21	20	oveq1d 6665	. . . . . . . 8 ⊢ (𝑥 = 𝑗 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))
22	21	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = 𝑗 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))
23	22	eqeq2d 2632	. . . . . 6 ⊢ (𝑥 = 𝑗 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
24	23	imbi2d 330	. . . . 5 ⊢ (𝑥 = 𝑗 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))))
25		zcn 11382	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ ℤ → 𝐿 ∈ ℂ)
26	25	mul02d 10234	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ ℤ → (0 · 𝐿) = 0)
27	26	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (0 · 𝐿) = 0)
28	27	adantr 481	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (0 · 𝐿) = 0)
29	28	oveq2d 6666	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + (0 · 𝐿)) = (𝐼 + 0))
30		elfzoelz 12470	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℤ)
31	30	zcnd 11483	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℂ)
32	31	addid1d 10236	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 + 0) = 𝐼)
33	32	ad2antll 765	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + 0) = 𝐼)
34	29, 33	eqtrd 2656	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + (0 · 𝐿)) = 𝐼)
35	34	oveq1d 6665	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)) = (𝐼 mod (#‘𝑊)))
36		zmodidfzoimp 12700	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 mod (#‘𝑊)) = 𝐼)
37	36	ad2antll 765	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 mod (#‘𝑊)) = 𝐼)
38	35, 37	eqtr2d 2657	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → 𝐼 = ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))
39	38	fveq2d 6195	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))
40		fveq1 6190	. . . . . . . . . . . . 13 ⊢ (𝑊 = (𝑊 cyclShift 𝐿) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
41	40	eqcoms 2630	. . . . . . . . . . . 12 ⊢ ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
42	41	ad2antrl 764	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
43	42	adantl 482	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
44		simprll 802	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → 𝑊 ∈ Word 𝑉)
45		simprlr 803	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → 𝐿 ∈ ℤ)
46		elfzo0 12508	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) ↔ (𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)))
47		nn0z 11400	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐼 ∈ ℕ₀ → 𝐼 ∈ ℤ)
48	47	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) → 𝐼 ∈ ℤ)
49		nn0z 11400	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ ℤ)
50		zmulcl 11426	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ)
51	49, 50	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℕ₀ ∧ 𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ)
52	51	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → (𝑦 · 𝐿) ∈ ℤ)
53		zaddcl 11417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ ℤ ∧ (𝑦 · 𝐿) ∈ ℤ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ)
54	48, 52, 53	syl2an 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ)
55		simplr 792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀)) → (#‘𝑊) ∈ ℕ)
56	54, 55	jca 554	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀)) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
57	56	ex 450	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
58	57	3adant3 1081	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
59	46, 58	sylbi 207	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
60	59	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
61	60	expd 452	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ₀ → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
62	61	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ ℤ → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑦 ∈ ℕ₀ → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
63	62	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑦 ∈ ℕ₀ → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
64	63	imp 445	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑦 ∈ ℕ₀ → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
65	64	impcom 446	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
66		zmodfzo 12693	. . . . . . . . . . . 12 ⊢ (((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))
67	65, 66	syl 17	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))
68		cshwidxmod 13549	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ ∧ ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))))
69	44, 45, 67, 68	syl3anc 1326	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))))
70		nn0re 11301	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℕ₀ → 𝐼 ∈ ℝ)
71		zre 11381	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
72		nn0re 11301	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ ℝ)
73		nnrp 11842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑊) ∈ ℕ → (#‘𝑊) ∈ ℝ⁺)
74		remulcl 10021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ)
75	74	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ)
76		readdcl 10019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 ∈ ℝ ∧ (𝑦 · 𝐿) ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
77	75, 76	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐼 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
78	77	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
79	78	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
80		simprll 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → 𝐿 ∈ ℝ)
81		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (#‘𝑊) ∈ ℝ⁺)
82		modaddmod 12709	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐼 + (𝑦 · 𝐿)) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ⁺) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)))
83	79, 80, 81, 82	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)))
84		recn 10026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐼 ∈ ℝ → 𝐼 ∈ ℂ)
85	84	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐼 ∈ ℂ)
86	74	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
87	86	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
88	87	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
89		recn 10026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐿 ∈ ℝ → 𝐿 ∈ ℂ)
90	89	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝐿 ∈ ℂ)
91	90	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐿 ∈ ℂ)
92	85, 88, 91	addassd 10062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 · 𝐿) + 𝐿)))
93		recn 10026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
94	93	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
95		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
96	94, 95, 90	adddird 10065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 + 1) · 𝐿) = ((𝑦 · 𝐿) + (1 · 𝐿)))
97	89	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐿 ∈ ℝ → (1 · 𝐿) = 𝐿)
98	97	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (1 · 𝐿) = 𝐿)
99	98	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + (1 · 𝐿)) = ((𝑦 · 𝐿) + 𝐿))
100	96, 99	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿))
101	100	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿))
102	101	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + ((𝑦 · 𝐿) + 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿)))
103	92, 102	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿)))
104	103	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿)))
105	104	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
106	83, 105	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((#‘𝑊) ∈ ℝ⁺ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
107	106	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑊) ∈ ℝ⁺ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
108	73, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((#‘𝑊) ∈ ℕ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
109	108	expd 452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
110	109	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
111	71, 72, 110	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
112	111	com13 88	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℝ → ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
113	70, 112	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ ℕ₀ → ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
114	113	imp 445	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
115	114	3adant3 1081	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
116	46, 115	sylbi 207	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
117	116	expd 452	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ₀ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
118	117	adantld 483	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (𝑦 ∈ ℕ₀ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
119	118	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (𝑦 ∈ ℕ₀ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
120	119	impcom 446	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑦 ∈ ℕ₀ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
121	120	impcom 446	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
122	121	fveq2d 6195	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
123	43, 69, 122	3eqtrd 2660	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
124	123	eqeq2d 2632	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
125	124	biimpd 219	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ₀ ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
126	125	ex 450	. . . . . 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 11472	. . . 4 ⊢ (𝑗 ∈ ℕ₀ → (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
129	128	com12 32	. . 3 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑗 ∈ ℕ₀ → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
130	129	ralrimiv 2965	. 2 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → ∀𝑗 ∈ ℕ₀ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))
131	130	ex 450	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ∀𝑗 ∈ ℕ₀ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℝ⁺crp 11832 ..^cfzo 12465 mod cmo 12668 #chash 13117 Word cword 13291 cyclShift ccsh 13534

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-hash 13118 df-word 13299 df-concat 13301 df-substr 13303 df-csh 13535

This theorem is referenced by: cshw1 13568 cshwsidrepsw 15800

W3C validator