Step | Hyp | Ref
| Expression |
1 | | ply1mulgsum.p |
. . 3
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | ply1mulgsum.b |
. . 3
⊢ 𝐵 = (Base‘𝑃) |
3 | | ply1mulgsum.a |
. . 3
⊢ 𝐴 = (coe1‘𝐾) |
4 | | ply1mulgsum.c |
. . 3
⊢ 𝐶 = (coe1‘𝐿) |
5 | | ply1mulgsum.x |
. . 3
⊢ 𝑋 = (var1‘𝑅) |
6 | | ply1mulgsum.pm |
. . 3
⊢ × =
(.r‘𝑃) |
7 | | ply1mulgsum.sm |
. . 3
⊢ · = (
·𝑠 ‘𝑃) |
8 | | ply1mulgsum.rm |
. . 3
⊢ ∗ =
(.r‘𝑅) |
9 | | ply1mulgsum.m |
. . 3
⊢ 𝑀 = (mulGrp‘𝑃) |
10 | | ply1mulgsum.e |
. . 3
⊢ ↑ =
(.g‘𝑀) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | ply1mulgsumlem1 41968 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑧 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) |
12 | | 2nn0 11186 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝑧 ∈ ℕ0
→ 2 ∈ ℕ0) |
14 | | id 22 |
. . . . . . 7
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℕ0) |
15 | 13, 14 | nn0mulcld 11233 |
. . . . . 6
⊢ (𝑧 ∈ ℕ0
→ (2 · 𝑧)
∈ ℕ0) |
16 | 15 | ad2antrr 758 |
. . . . 5
⊢ (((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → (2 · 𝑧) ∈
ℕ0) |
17 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑠 = (2 · 𝑧) → (𝑠 < 𝑛 ↔ (2 · 𝑧) < 𝑛)) |
18 | 17 | imbi1d 330 |
. . . . . . 7
⊢ (𝑠 = (2 · 𝑧) → ((𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)) ↔ ((2 · 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)))) |
19 | 18 | ralbidv 2969 |
. . . . . 6
⊢ (𝑠 = (2 · 𝑧) → (∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)) ↔ ∀𝑛 ∈ ℕ0 ((2
· 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)))) |
20 | 19 | adantl 481 |
. . . . 5
⊢ ((((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑠 = (2 · 𝑧)) → (∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)) ↔ ∀𝑛 ∈ ℕ0 ((2
· 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)))) |
21 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ ℕ0
→ 2 ∈ ℝ) |
23 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℝ) |
24 | 22, 23 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ ℕ0
→ (2 · 𝑧)
∈ ℝ) |
25 | 24 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (2 · 𝑧) ∈ ℝ) |
26 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℝ) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑛 ∈ ℝ) |
29 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑙 ∈ (0...𝑛) → 𝑙 ∈ ℕ0) |
30 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑙 ∈ ℕ0
→ 𝑙 ∈
ℝ) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 ∈ (0...𝑛) → 𝑙 ∈ ℝ) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑙 ∈ ℝ) |
33 | 25, 28, 32 | ltsub1d 10515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) < 𝑛 ↔ ((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙))) |
34 | 23 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑧 ∈ ℝ) |
35 | 32, 34, 25 | lesub2d 10514 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑙 ≤ 𝑧 ↔ ((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙))) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ ((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙)) → (𝑙 ≤ 𝑧 ↔ ((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙))) |
37 | 24, 23 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ ℕ0
→ ((2 · 𝑧)
− 𝑧) ∈
ℝ) |
38 | 37 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) − 𝑧) ∈ ℝ) |
39 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (2 · 𝑧) ∈ ℝ) |
40 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((2
· 𝑧) ∈ ℝ
∧ 𝑙 ∈ ℝ)
→ ((2 · 𝑧)
− 𝑙) ∈
ℝ) |
41 | 39, 31, 40 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) − 𝑙) ∈ ℝ) |
42 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑛 ∈ ℝ ∧ 𝑙 ∈ ℝ) → (𝑛 − 𝑙) ∈ ℝ) |
43 | 27, 31, 42 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑛 − 𝑙) ∈ ℝ) |
44 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((2
· 𝑧) − 𝑧) ∈ ℝ ∧ ((2
· 𝑧) − 𝑙) ∈ ℝ ∧ (𝑛 − 𝑙) ∈ ℝ) → ((((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) ∧ ((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙)) → ((2 · 𝑧) − 𝑧) < (𝑛 − 𝑙))) |
45 | 38, 41, 43, 44 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) ∧ ((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙)) → ((2 · 𝑧) − 𝑧) < (𝑛 − 𝑙))) |
46 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℂ) |
47 | | 2txmxeqx 11026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ ℂ → ((2
· 𝑧) − 𝑧) = 𝑧) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ ℕ0
→ ((2 · 𝑧)
− 𝑧) = 𝑧) |
49 | 48 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) − 𝑧) = 𝑧) |
50 | 49 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (((2 · 𝑧) − 𝑧) < (𝑛 − 𝑙) ↔ 𝑧 < (𝑛 − 𝑙))) |
51 | 45, 50 | sylibd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) ∧ ((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙)) → 𝑧 < (𝑛 − 𝑙))) |
52 | 51 | expcomd 453 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙) → (((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) → 𝑧 < (𝑛 − 𝑙)))) |
53 | 52 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ ((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙)) → (((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) → 𝑧 < (𝑛 − 𝑙))) |
54 | 36, 53 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ ((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙)) → (𝑙 ≤ 𝑧 → 𝑧 < (𝑛 − 𝑙))) |
55 | 54 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (((2 · 𝑧) − 𝑙) < (𝑛 − 𝑙) → (𝑙 ≤ 𝑧 → 𝑧 < (𝑛 − 𝑙)))) |
56 | 33, 55 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) < 𝑛 → (𝑙 ≤ 𝑧 → 𝑧 < (𝑛 − 𝑙)))) |
57 | 56 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (𝑙 ∈ (0...𝑛) → ((2 · 𝑧) < 𝑛 → (𝑙 ≤ 𝑧 → 𝑧 < (𝑛 − 𝑙))))) |
58 | 57 | com23 84 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((2 · 𝑧) < 𝑛 → (𝑙 ∈ (0...𝑛) → (𝑙 ≤ 𝑧 → 𝑧 < (𝑛 − 𝑙))))) |
59 | 58 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℕ0
→ (𝑛 ∈
ℕ0 → ((2 · 𝑧) < 𝑛 → (𝑙 ∈ (0...𝑛) → (𝑙 ≤ 𝑧 → 𝑧 < (𝑛 − 𝑙)))))) |
60 | 59 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → (𝑛 ∈ ℕ0 → ((2
· 𝑧) < 𝑛 → (𝑙 ∈ (0...𝑛) → (𝑙 ≤ 𝑧 → 𝑧 < (𝑛 − 𝑙)))))) |
61 | 60 | imp41 617 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝑙 ≤ 𝑧 → 𝑧 < (𝑛 − 𝑙))) |
62 | 61 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → 𝑧 < (𝑛 − 𝑙)) |
63 | | fznn0sub2 12315 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 ∈ (0...𝑛) → (𝑛 − 𝑙) ∈ (0...𝑛)) |
64 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 − 𝑙) ∈ (0...𝑛) → (𝑛 − 𝑙) ∈
ℕ0) |
65 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑛 − 𝑙) → (𝑧 < 𝑥 ↔ 𝑧 < (𝑛 − 𝑙))) |
66 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (𝑛 − 𝑙) → (𝐴‘𝑥) = (𝐴‘(𝑛 − 𝑙))) |
67 | 66 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (𝑛 − 𝑙) → ((𝐴‘𝑥) = (0g‘𝑅) ↔ (𝐴‘(𝑛 − 𝑙)) = (0g‘𝑅))) |
68 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (𝑛 − 𝑙) → (𝐶‘𝑥) = (𝐶‘(𝑛 − 𝑙))) |
69 | 68 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (𝑛 − 𝑙) → ((𝐶‘𝑥) = (0g‘𝑅) ↔ (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅))) |
70 | 67, 69 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑛 − 𝑙) → (((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)) ↔ ((𝐴‘(𝑛 − 𝑙)) = (0g‘𝑅) ∧ (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)))) |
71 | 65, 70 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑛 − 𝑙) → ((𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) ↔ (𝑧 < (𝑛 − 𝑙) → ((𝐴‘(𝑛 − 𝑙)) = (0g‘𝑅) ∧ (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅))))) |
72 | 71 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 − 𝑙) ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) → (𝑧 < (𝑛 − 𝑙) → ((𝐴‘(𝑛 − 𝑙)) = (0g‘𝑅) ∧ (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)))) |
73 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴‘(𝑛 − 𝑙)) = (0g‘𝑅) ∧ (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)) |
74 | 72, 73 | syl6 34 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 − 𝑙) ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) → (𝑧 < (𝑛 − 𝑙) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅))) |
75 | 74 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 − 𝑙) ∈ ℕ0 →
(∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) → (𝑧 < (𝑛 − 𝑙) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)))) |
76 | 63, 64, 75 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 ∈ (0...𝑛) → (∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) → (𝑧 < (𝑛 − 𝑙) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)))) |
77 | 76 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) → (𝑙 ∈ (0...𝑛) → (𝑧 < (𝑛 − 𝑙) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)))) |
78 | 77 | ad4antlr 765 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → (𝑙 ∈ (0...𝑛) → (𝑧 < (𝑛 − 𝑙) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)))) |
79 | 78 | imp 444 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝑧 < (𝑛 − 𝑙) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅))) |
80 | 79 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝑧 < (𝑛 − 𝑙) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅))) |
81 | 62, 80 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐶‘(𝑛 − 𝑙)) = (0g‘𝑅)) |
82 | 81 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))) = ((𝐴‘𝑙) ∗
(0g‘𝑅))) |
83 | | simplr1 1096 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring) |
84 | 83 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → 𝑅 ∈ Ring) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → 𝑅 ∈ Ring) |
86 | | simplr2 1097 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝐾 ∈ 𝐵) |
87 | 86 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → 𝐾 ∈ 𝐵) |
88 | 87, 29 | anim12i 588 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝐾 ∈ 𝐵 ∧ 𝑙 ∈
ℕ0)) |
89 | 88 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐾 ∈ 𝐵 ∧ 𝑙 ∈
ℕ0)) |
90 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅) =
(Base‘𝑅) |
91 | 3, 2, 1, 90 | coe1fvalcl 19403 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑙 ∈ ℕ0) → (𝐴‘𝑙) ∈ (Base‘𝑅)) |
92 | 89, 91 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐴‘𝑙) ∈ (Base‘𝑅)) |
93 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑅) = (0g‘𝑅) |
94 | 90, 8, 93 | ringrz 18411 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝐴‘𝑙) ∈ (Base‘𝑅)) → ((𝐴‘𝑙) ∗
(0g‘𝑅)) =
(0g‘𝑅)) |
95 | 85, 92, 94 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴‘𝑙) ∗
(0g‘𝑅)) =
(0g‘𝑅)) |
96 | 82, 95 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))) = (0g‘𝑅)) |
97 | | ltnle 9996 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℝ ∧ 𝑙 ∈ ℝ) → (𝑧 < 𝑙 ↔ ¬ 𝑙 ≤ 𝑧)) |
98 | 23, 30, 97 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ ℕ0
∧ 𝑙 ∈
ℕ0) → (𝑧 < 𝑙 ↔ ¬ 𝑙 ≤ 𝑧)) |
99 | 98 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℕ0
∧ 𝑙 ∈
ℕ0) → (¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙)) |
100 | 99 | expcom 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 ∈ ℕ0
→ (𝑧 ∈
ℕ0 → (¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙))) |
101 | 29, 100 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 ∈ (0...𝑛) → (𝑧 ∈ ℕ0 → (¬
𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙))) |
102 | 101 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℕ0
→ (𝑙 ∈ (0...𝑛) → (¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙))) |
103 | 102 | ad4antr 764 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → (𝑙 ∈ (0...𝑛) → (¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙))) |
104 | 103 | imp 444 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙)) |
105 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑙 → (𝑧 < 𝑥 ↔ 𝑧 < 𝑙)) |
106 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑙 → (𝐴‘𝑥) = (𝐴‘𝑙)) |
107 | 106 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑙 → ((𝐴‘𝑥) = (0g‘𝑅) ↔ (𝐴‘𝑙) = (0g‘𝑅))) |
108 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑙 → (𝐶‘𝑥) = (𝐶‘𝑙)) |
109 | 108 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑙 → ((𝐶‘𝑥) = (0g‘𝑅) ↔ (𝐶‘𝑙) = (0g‘𝑅))) |
110 | 107, 109 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑙 → (((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)) ↔ ((𝐴‘𝑙) = (0g‘𝑅) ∧ (𝐶‘𝑙) = (0g‘𝑅)))) |
111 | 105, 110 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑙 → ((𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) ↔ (𝑧 < 𝑙 → ((𝐴‘𝑙) = (0g‘𝑅) ∧ (𝐶‘𝑙) = (0g‘𝑅))))) |
112 | 111 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑙 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) → (𝑧 < 𝑙 → ((𝐴‘𝑙) = (0g‘𝑅) ∧ (𝐶‘𝑙) = (0g‘𝑅)))) |
113 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴‘𝑙) = (0g‘𝑅) ∧ (𝐶‘𝑙) = (0g‘𝑅)) → (𝐴‘𝑙) = (0g‘𝑅)) |
114 | 112, 113 | syl6 34 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑙 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) → (𝑧 < 𝑙 → (𝐴‘𝑙) = (0g‘𝑅))) |
115 | 114 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) → (𝑧 < 𝑙 → (𝐴‘𝑙) = (0g‘𝑅)))) |
116 | 29, 115 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 ∈ (0...𝑛) → (∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) → (𝑧 < 𝑙 → (𝐴‘𝑙) = (0g‘𝑅)))) |
117 | 116 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) → (𝑙 ∈ (0...𝑛) → (𝑧 < 𝑙 → (𝐴‘𝑙) = (0g‘𝑅)))) |
118 | 117 | ad4antlr 765 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → (𝑙 ∈ (0...𝑛) → (𝑧 < 𝑙 → (𝐴‘𝑙) = (0g‘𝑅)))) |
119 | 118 | imp 444 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝑧 < 𝑙 → (𝐴‘𝑙) = (0g‘𝑅))) |
120 | 104, 119 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (¬ 𝑙 ≤ 𝑧 → (𝐴‘𝑙) = (0g‘𝑅))) |
121 | 120 | impcom 445 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐴‘𝑙) = (0g‘𝑅)) |
122 | 121 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((¬
𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))) = ((0g‘𝑅) ∗ (𝐶‘(𝑛 − 𝑙)))) |
123 | 84 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → 𝑅 ∈ Ring) |
124 | | simplr3 1098 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝐿 ∈ 𝐵) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → 𝐿 ∈ 𝐵) |
126 | | fznn0sub 12244 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ (0...𝑛) → (𝑛 − 𝑙) ∈
ℕ0) |
127 | 125, 126 | anim12i 588 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝐿 ∈ 𝐵 ∧ (𝑛 − 𝑙) ∈
ℕ0)) |
128 | 127 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐿 ∈ 𝐵 ∧ (𝑛 − 𝑙) ∈
ℕ0)) |
129 | 4, 2, 1, 90 | coe1fvalcl 19403 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ 𝐵 ∧ (𝑛 − 𝑙) ∈ ℕ0) → (𝐶‘(𝑛 − 𝑙)) ∈ (Base‘𝑅)) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐶‘(𝑛 − 𝑙)) ∈ (Base‘𝑅)) |
131 | 90, 8, 93 | ringlz 18410 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝐶‘(𝑛 − 𝑙)) ∈ (Base‘𝑅)) → ((0g‘𝑅) ∗ (𝐶‘(𝑛 − 𝑙))) = (0g‘𝑅)) |
132 | 123, 130,
131 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((¬
𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((0g‘𝑅) ∗ (𝐶‘(𝑛 − 𝑙))) = (0g‘𝑅)) |
133 | 122, 132 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((¬
𝑙 ≤ 𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))) = (0g‘𝑅)) |
134 | 96, 133 | pm2.61ian 827 |
. . . . . . . . . 10
⊢
((((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))) = (0g‘𝑅)) |
135 | 134 | mpteq2dva 4672 |
. . . . . . . . 9
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ (0g‘𝑅))) |
136 | 135 | oveq2d 6565 |
. . . . . . . 8
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ (0g‘𝑅)))) |
137 | | ringmnd 18379 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
138 | 137 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑅 ∈ Mnd) |
139 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(0...𝑛) ∈
V |
140 | 138, 139 | jctir 559 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑅 ∈ Mnd ∧ (0...𝑛) ∈ V)) |
141 | 140 | ad3antlr 763 |
. . . . . . . . 9
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → (𝑅 ∈ Mnd ∧ (0...𝑛) ∈ V)) |
142 | 93 | gsumz 17197 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ (0...𝑛) ∈ V) → (𝑅 Σg
(𝑙 ∈ (0...𝑛) ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
143 | 141, 142 | syl 17 |
. . . . . . . 8
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ (0g‘𝑅))) = (0g‘𝑅)) |
144 | 136, 143 | eqtrd 2644 |
. . . . . . 7
⊢
(((((𝑧 ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2
· 𝑧) < 𝑛) → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)) |
145 | 144 | ex 449 |
. . . . . 6
⊢ ((((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((2
· 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅))) |
146 | 145 | ralrimiva 2949 |
. . . . 5
⊢ (((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → ∀𝑛 ∈ ℕ0 ((2 ·
𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅))) |
147 | 16, 20, 146 | rspcedvd 3289 |
. . . 4
⊢ (((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅))) |
148 | 147 | ex 449 |
. . 3
⊢ ((𝑧 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑧 <
𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅)))) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)))) |
149 | 148 | rexlimiva 3010 |
. 2
⊢
(∃𝑧 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴‘𝑥) = (0g‘𝑅) ∧ (𝐶‘𝑥) = (0g‘𝑅))) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)))) |
150 | 11, 149 | mpcom 37 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅))) |