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

Theorem cshweqrep 13367
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..^(#‘𝑊))) → ∀𝑗 ∈ ℕ0 (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
Distinct variable groups:   𝑗,𝐼   𝑗,𝐿   𝑗,𝑉   𝑗,𝑊

Proof of Theorem cshweqrep
Dummy variables 𝑦 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6534 . . . . . . . . . 10 (𝑥 = 0 → (𝑥 · 𝐿) = (0 · 𝐿))
21oveq2d 6543 . . . . . . . . 9 (𝑥 = 0 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (0 · 𝐿)))
32oveq1d 6542 . . . . . . . 8 (𝑥 = 0 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))
43fveq2d 6092 . . . . . . 7 (𝑥 = 0 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))
54eqeq2d 2619 . . . . . 6 (𝑥 = 0 → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))))
65imbi2d 328 . . . . 5 (𝑥 = 0 → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))))
7 oveq1 6534 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 · 𝐿) = (𝑦 · 𝐿))
87oveq2d 6543 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑦 · 𝐿)))
98oveq1d 6542 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))
109fveq2d 6092 . . . . . . 7 (𝑥 = 𝑦 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
1110eqeq2d 2619 . . . . . 6 (𝑥 = 𝑦 → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))))
1211imbi2d 328 . . . . 5 (𝑥 = 𝑦 → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))))
13 oveq1 6534 . . . . . . . . . 10 (𝑥 = (𝑦 + 1) → (𝑥 · 𝐿) = ((𝑦 + 1) · 𝐿))
1413oveq2d 6543 . . . . . . . . 9 (𝑥 = (𝑦 + 1) → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿)))
1514oveq1d 6542 . . . . . . . 8 (𝑥 = (𝑦 + 1) → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
1615fveq2d 6092 . . . . . . 7 (𝑥 = (𝑦 + 1) → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
1716eqeq2d 2619 . . . . . 6 (𝑥 = (𝑦 + 1) → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
1817imbi2d 328 . . . . 5 (𝑥 = (𝑦 + 1) → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
19 oveq1 6534 . . . . . . . . . 10 (𝑥 = 𝑗 → (𝑥 · 𝐿) = (𝑗 · 𝐿))
2019oveq2d 6543 . . . . . . . . 9 (𝑥 = 𝑗 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑗 · 𝐿)))
2120oveq1d 6542 . . . . . . . 8 (𝑥 = 𝑗 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))
2221fveq2d 6092 . . . . . . 7 (𝑥 = 𝑗 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))
2322eqeq2d 2619 . . . . . 6 (𝑥 = 𝑗 → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
2423imbi2d 328 . . . . 5 (𝑥 = 𝑗 → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))))
25 zcn 11218 . . . . . . . . . . . . 13 (𝐿 ∈ ℤ → 𝐿 ∈ ℂ)
2625mul02d 10086 . . . . . . . . . . . 12 (𝐿 ∈ ℤ → (0 · 𝐿) = 0)
2726adantl 480 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (0 · 𝐿) = 0)
2827adantr 479 . . . . . . . . . 10 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (0 · 𝐿) = 0)
2928oveq2d 6543 . . . . . . . . 9 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + (0 · 𝐿)) = (𝐼 + 0))
30 elfzoelz 12297 . . . . . . . . . . . 12 (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℤ)
3130zcnd 11318 . . . . . . . . . . 11 (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℂ)
3231addid1d 10088 . . . . . . . . . 10 (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 + 0) = 𝐼)
3332ad2antll 760 . . . . . . . . 9 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + 0) = 𝐼)
3429, 33eqtrd 2643 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + (0 · 𝐿)) = 𝐼)
3534oveq1d 6542 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)) = (𝐼 mod (#‘𝑊)))
36 zmodidfzoimp 12520 . . . . . . . 8 (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 mod (#‘𝑊)) = 𝐼)
3736ad2antll 760 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 mod (#‘𝑊)) = 𝐼)
3835, 37eqtr2d 2644 . . . . . 6 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → 𝐼 = ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))
3938fveq2d 6092 . . . . 5 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))
40 fveq1 6087 . . . . . . . . . . . . 13 (𝑊 = (𝑊 cyclShift 𝐿) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
4140eqcoms 2617 . . . . . . . . . . . 12 ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
4241ad2antrl 759 . . . . . . . . . . 11 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
4342adantl 480 . . . . . . . . . 10 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
44 simprll 797 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → 𝑊 ∈ Word 𝑉)
45 simprlr 798 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → 𝐿 ∈ ℤ)
46 elfzo0 12334 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (0..^(#‘𝑊)) ↔ (𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)))
47 nn0z 11236 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐼 ∈ ℕ0𝐼 ∈ ℤ)
4847adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) → 𝐼 ∈ ℤ)
49 nn0z 11236 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℕ0𝑦 ∈ ℤ)
50 zmulcl 11262 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ)
5149, 50sylan 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℕ0𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ)
5251ancoms 467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → (𝑦 · 𝐿) ∈ ℤ)
53 zaddcl 11253 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐼 ∈ ℤ ∧ (𝑦 · 𝐿) ∈ ℤ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ)
5448, 52, 53syl2an 492 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ)
55 simplr 787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0)) → (#‘𝑊) ∈ ℕ)
5654, 55jca 552 . . . . . . . . . . . . . . . . . . . . 21 (((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0)) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
5756ex 448 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
58573adant3 1073 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
5946, 58sylbi 205 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
6059adantl 480 . . . . . . . . . . . . . . . . 17 (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
6160expd 450 . . . . . . . . . . . . . . . 16 (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
6261com12 32 . . . . . . . . . . . . . . 15 (𝐿 ∈ ℤ → (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
6362adantl 480 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
6463imp 443 . . . . . . . . . . . . 13 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
6564impcom 444 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
66 zmodfzo 12513 . . . . . . . . . . . 12 (((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))
6765, 66syl 17 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))
68 cshwidxmod 13349 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ∧ ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))))
6944, 45, 67, 68syl3anc 1317 . . . . . . . . . 10 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))))
70 nn0re 11151 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ ℕ0𝐼 ∈ ℝ)
71 zre 11217 . . . . . . . . . . . . . . . . . . . . . 22 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
72 nn0re 11151 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
73 nnrp 11677 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑊) ∈ ℕ → (#‘𝑊) ∈ ℝ+)
74 remulcl 9878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ)
7574ancoms 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ)
76 readdcl 9876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐼 ∈ ℝ ∧ (𝑦 · 𝐿) ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
7775, 76sylan2 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐼 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
7877ancoms 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
7978adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
80 simprll 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → 𝐿 ∈ ℝ)
81 simpl 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (#‘𝑊) ∈ ℝ+)
82 modaddmod 12529 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐼 + (𝑦 · 𝐿)) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ+) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)))
8379, 80, 81, 82syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)))
84 recn 9883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐼 ∈ ℝ → 𝐼 ∈ ℂ)
8584adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐼 ∈ ℂ)
8674recnd 9925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
8786ancoms 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
8887adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
89 recn 9883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐿 ∈ ℝ → 𝐿 ∈ ℂ)
9089adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝐿 ∈ ℂ)
9190adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐿 ∈ ℂ)
9285, 88, 91addassd 9919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 · 𝐿) + 𝐿)))
93 recn 9883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
9493adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
95 1cnd 9913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
9694, 95, 90adddird 9922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 + 1) · 𝐿) = ((𝑦 · 𝐿) + (1 · 𝐿)))
9789mulid2d 9915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐿 ∈ ℝ → (1 · 𝐿) = 𝐿)
9897adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (1 · 𝐿) = 𝐿)
9998oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + (1 · 𝐿)) = ((𝑦 · 𝐿) + 𝐿))
10096, 99eqtr2d 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿))
101100adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿))
102101oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + ((𝑦 · 𝐿) + 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿)))
10392, 102eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿)))
104103adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿)))
105104oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
10683, 105eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
107106ex 448 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑊) ∈ ℝ+ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
10873, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((#‘𝑊) ∈ ℕ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
109108expd 450 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
110109com12 32 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
11171, 72, 110syl2an 492 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
112111com13 85 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ ℝ → ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
11370, 112syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ ℕ0 → ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
114113imp 443 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
1151143adant3 1073 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
11646, 115sylbi 205 . . . . . . . . . . . . . . . 16 (𝐼 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
117116expd 450 . . . . . . . . . . . . . . 15 (𝐼 ∈ (0..^(#‘𝑊)) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
118117adantld 481 . . . . . . . . . . . . . 14 (𝐼 ∈ (0..^(#‘𝑊)) → ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
119118adantl 480 . . . . . . . . . . . . 13 (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
120119impcom 444 . . . . . . . . . . . 12 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
121120impcom 444 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
122121fveq2d 6092 . . . . . . . . . 10 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
12343, 69, 1223eqtrd 2647 . . . . . . . . 9 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
124123eqeq2d 2619 . . . . . . . 8 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
125124biimpd 217 . . . . . . 7 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) → (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
126125ex 448 . . . . . 6 (𝑦 ∈ ℕ0 → (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) → (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
127126a2d 29 . . . . 5 (𝑦 ∈ ℕ0 → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))) → (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
1286, 12, 18, 24, 39, 127nn0ind 11307 . . . 4 (𝑗 ∈ ℕ0 → (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
129128com12 32 . . 3 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑗 ∈ ℕ0 → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
130129ralrimiv 2947 . 2 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → ∀𝑗 ∈ ℕ0 (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))
131130ex 448 1 ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → ∀𝑗 ∈ ℕ0 (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895   class class class wbr 4577  cfv 5790  (class class class)co 6527  cc 9791  cr 9792  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798   < clt 9931  cn 10870  0cn0 11142  cz 11213  +crp 11667  ..^cfzo 12292   mod cmo 12488  #chash 12937  Word cword 13095   cyclShift ccsh 13334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-oadd 7429  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-sup 8209  df-inf 8210  df-card 8626  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-n0 11143  df-z 11214  df-uz 11523  df-rp 11668  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-hash 12938  df-word 13103  df-concat 13105  df-substr 13107  df-csh 13335
This theorem is referenced by:  cshw1  13368  cshwsidrepsw  15587
  Copyright terms: Public domain W3C validator