Step | Hyp | Ref
| Expression |
1 | | coe1tmmul.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | | coe1tmmul.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝐾) |
3 | | coe1tmmul.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
4 | | coe1tm.k |
. . . . 5
⊢ 𝐾 = (Base‘𝑅) |
5 | | coe1tm.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
6 | | coe1tm.x |
. . . . 5
⊢ 𝑋 = (var1‘𝑅) |
7 | | coe1tm.m |
. . . . 5
⊢ · = (
·𝑠 ‘𝑃) |
8 | | coe1tm.n |
. . . . 5
⊢ 𝑁 = (mulGrp‘𝑃) |
9 | | coe1tm.e |
. . . . 5
⊢ ↑ =
(.g‘𝑁) |
10 | | coe1tmmul.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑃) |
11 | 4, 5, 6, 7, 8, 9, 10 | ply1tmcl 19463 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) |
12 | 1, 2, 3, 11 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) |
13 | | coe1tmmul.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
14 | | coe1tmmul.t |
. . . 4
⊢ ∙ =
(.r‘𝑃) |
15 | | coe1tmmul.u |
. . . 4
⊢ × =
(.r‘𝑅) |
16 | 5, 14, 15, 10 | coe1mul 19461 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵 ∧ 𝐴 ∈ 𝐵) → (coe1‘((𝐶 · (𝐷 ↑ 𝑋)) ∙ 𝐴)) = (𝑥 ∈ ℕ0 ↦ (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))))) |
17 | 1, 12, 13, 16 | syl3anc 1318 |
. 2
⊢ (𝜑 →
(coe1‘((𝐶
·
(𝐷 ↑ 𝑋)) ∙ 𝐴)) = (𝑥 ∈ ℕ0 ↦ (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))))) |
18 | | eqeq2 2621 |
. . . 4
⊢ ((𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))) = if(𝐷 ≤ 𝑥, (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))), 0 ) → ((𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))) ↔ (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = if(𝐷 ≤ 𝑥, (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))), 0 ))) |
19 | | eqeq2 2621 |
. . . 4
⊢ ( 0 = if(𝐷 ≤ 𝑥, (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))), 0 ) → ((𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = 0 ↔ (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = if(𝐷 ≤ 𝑥, (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))), 0 ))) |
20 | | coe1tm.z |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
21 | 1 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → 𝑅 ∈ Ring) |
22 | | ringmnd 18379 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → 𝑅 ∈ Mnd) |
24 | | ovex 6577 |
. . . . . . 7
⊢
(0...𝑥) ∈
V |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → (0...𝑥) ∈ V) |
26 | 3 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → 𝐷 ∈
ℕ0) |
27 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → 𝐷 ≤ 𝑥) |
28 | | fznn0 12301 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ (𝐷 ∈ (0...𝑥) ↔ (𝐷 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥))) |
29 | 28 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → (𝐷 ∈ (0...𝑥) ↔ (𝐷 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥))) |
30 | 26, 27, 29 | mpbir2and 959 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → 𝐷 ∈ (0...𝑥)) |
31 | 1 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) → 𝑅 ∈ Ring) |
32 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(coe1‘(𝐶 · (𝐷 ↑ 𝑋))) = (coe1‘(𝐶 · (𝐷 ↑ 𝑋))) |
33 | 32, 10, 5, 4 | coe1f 19402 |
. . . . . . . . . . . 12
⊢ ((𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵 → (coe1‘(𝐶 · (𝐷 ↑ 𝑋))):ℕ0⟶𝐾) |
34 | 12, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
(coe1‘(𝐶
·
(𝐷 ↑ 𝑋))):ℕ0⟶𝐾) |
35 | 34 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) →
(coe1‘(𝐶
·
(𝐷 ↑ 𝑋))):ℕ0⟶𝐾) |
36 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0...𝑥) → 𝑦 ∈ ℕ0) |
37 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢
(((coe1‘(𝐶 · (𝐷 ↑ 𝑋))):ℕ0⟶𝐾 ∧ 𝑦 ∈ ℕ0) →
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝑦) ∈ 𝐾) |
38 | 35, 36, 37 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ∈ 𝐾) |
39 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(coe1‘𝐴) = (coe1‘𝐴) |
40 | 39, 10, 5, 4 | coe1f 19402 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝐵 → (coe1‘𝐴):ℕ0⟶𝐾) |
41 | 13, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
(coe1‘𝐴):ℕ0⟶𝐾) |
42 | 41 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) →
(coe1‘𝐴):ℕ0⟶𝐾) |
43 | | fznn0sub 12244 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0...𝑥) → (𝑥 − 𝑦) ∈
ℕ0) |
44 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢
(((coe1‘𝐴):ℕ0⟶𝐾 ∧ (𝑥 − 𝑦) ∈ ℕ0) →
((coe1‘𝐴)‘(𝑥 − 𝑦)) ∈ 𝐾) |
45 | 42, 43, 44 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) → ((coe1‘𝐴)‘(𝑥 − 𝑦)) ∈ 𝐾) |
46 | 4, 15 | ringcl 18384 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝑦) ∈ 𝐾 ∧ ((coe1‘𝐴)‘(𝑥 − 𝑦)) ∈ 𝐾) → (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) ∈ 𝐾) |
47 | 31, 38, 45, 46 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) → (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) ∈ 𝐾) |
48 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))) = (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))) |
49 | 47, 48 | fmptd 6292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))):(0...𝑥)⟶𝐾) |
50 | 49 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))):(0...𝑥)⟶𝐾) |
51 | 1 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → 𝑅 ∈ Ring) |
52 | 2 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → 𝐶 ∈ 𝐾) |
53 | 3 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → 𝐷 ∈
ℕ0) |
54 | | eldifi 3694 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((0...𝑥) ∖ {𝐷}) → 𝑦 ∈ (0...𝑥)) |
55 | 54, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((0...𝑥) ∖ {𝐷}) → 𝑦 ∈ ℕ0) |
56 | 55 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → 𝑦 ∈ ℕ0) |
57 | | eldifsni 4261 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((0...𝑥) ∖ {𝐷}) → 𝑦 ≠ 𝐷) |
58 | 57 | necomd 2837 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((0...𝑥) ∖ {𝐷}) → 𝐷 ≠ 𝑦) |
59 | 58 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → 𝐷 ≠ 𝑦) |
60 | 20, 4, 5, 6, 7, 8, 9, 51, 52, 53, 56, 59 | coe1tmfv2 19466 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) = 0 ) |
61 | 60 | oveq1d 6564 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = ( 0 ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))) |
62 | 4, 15, 20 | ringlz 18410 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
((coe1‘𝐴)‘(𝑥 − 𝑦)) ∈ 𝐾) → ( 0 ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = 0 ) |
63 | 31, 45, 62 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) → ( 0 ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = 0 ) |
64 | 54, 63 | sylan2 490 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → ( 0 ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = 0 ) |
65 | 64 | adantlr 747 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → ( 0 ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = 0 ) |
66 | 61, 65 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) ∧ 𝑦 ∈ ((0...𝑥) ∖ {𝐷})) → (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = 0 ) |
67 | 66, 25 | suppss2 7216 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))) supp 0 ) ⊆ {𝐷}) |
68 | 4, 20, 23, 25, 30, 50, 67 | gsumpt 18184 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))‘𝐷)) |
69 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝐷 → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) = ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷)) |
70 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐷 → (𝑥 − 𝑦) = (𝑥 − 𝐷)) |
71 | 70 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑦 = 𝐷 → ((coe1‘𝐴)‘(𝑥 − 𝑦)) = ((coe1‘𝐴)‘(𝑥 − 𝐷))) |
72 | 69, 71 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑦 = 𝐷 → (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷) ×
((coe1‘𝐴)‘(𝑥 − 𝐷)))) |
73 | | ovex 6577 |
. . . . . . . 8
⊢
(((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷) ×
((coe1‘𝐴)‘(𝑥 − 𝐷))) ∈ V |
74 | 72, 48, 73 | fvmpt 6191 |
. . . . . . 7
⊢ (𝐷 ∈ (0...𝑥) → ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))‘𝐷) = (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷) ×
((coe1‘𝐴)‘(𝑥 − 𝐷)))) |
75 | 30, 74 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))‘𝐷) = (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷) ×
((coe1‘𝐴)‘(𝑥 − 𝐷)))) |
76 | 20, 4, 5, 6, 7, 8, 9 | coe1tmfv1 19465 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝐷) = 𝐶) |
77 | 1, 2, 3, 76 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 →
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝐷) = 𝐶) |
78 | 77 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷) = 𝐶) |
79 | 78 | oveq1d 6564 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷) ×
((coe1‘𝐴)‘(𝑥 − 𝐷))) = (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷)))) |
80 | 75, 79 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))‘𝐷) = (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷)))) |
81 | 68, 80 | eqtrd 2644 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷)))) |
82 | 1 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → 𝑅 ∈ Ring) |
83 | 2 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → 𝐶 ∈ 𝐾) |
84 | 3 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → 𝐷 ∈
ℕ0) |
85 | 36 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → 𝑦 ∈ ℕ0) |
86 | | elfzle2 12216 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0...𝑥) → 𝑦 ≤ 𝑥) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) → 𝑦 ≤ 𝑥) |
88 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝐷 = 𝑦 → (𝐷 ≤ 𝑥 ↔ 𝑦 ≤ 𝑥)) |
89 | 87, 88 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) → (𝐷 = 𝑦 → 𝐷 ≤ 𝑥)) |
90 | 89 | necon3bd 2796 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) → (¬ 𝐷 ≤ 𝑥 → 𝐷 ≠ 𝑦)) |
91 | 90 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ (0...𝑥)) ∧ ¬ 𝐷 ≤ 𝑥) → 𝐷 ≠ 𝑦) |
92 | 91 | an32s 842 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → 𝐷 ≠ 𝑦) |
93 | 20, 4, 5, 6, 7, 8, 9, 82, 83, 84, 85, 92 | coe1tmfv2 19466 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) = 0 ) |
94 | 93 | oveq1d 6564 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = ( 0 ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))) |
95 | 63 | adantlr 747 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → ( 0 ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = 0 ) |
96 | 94, 95 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))) = 0 ) |
97 | 96 | mpteq2dva 4672 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))) = (𝑦 ∈ (0...𝑥) ↦ 0 )) |
98 | 97 | oveq2d 6565 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ 0 ))) |
99 | 1, 22 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Mnd) |
100 | 99 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → 𝑅 ∈ Mnd) |
101 | 24 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (0...𝑥) ∈ V) |
102 | 20 | gsumz 17197 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ (0...𝑥) ∈ V) → (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦ 0 )) = 0 ) |
103 | 100, 101,
102 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ 0 )) = 0 ) |
104 | 98, 103 | eqtrd 2644 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = 0 ) |
105 | 18, 19, 81, 104 | ifbothda 4073 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦))))) = if(𝐷 ≤ 𝑥, (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))), 0 )) |
106 | 105 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℕ0 ↦ (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝑦) ×
((coe1‘𝐴)‘(𝑥 − 𝑦)))))) = (𝑥 ∈ ℕ0 ↦ if(𝐷 ≤ 𝑥, (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))), 0 ))) |
107 | 17, 106 | eqtrd 2644 |
1
⊢ (𝜑 →
(coe1‘((𝐶
·
(𝐷 ↑ 𝑋)) ∙ 𝐴)) = (𝑥 ∈ ℕ0 ↦ if(𝐷 ≤ 𝑥, (𝐶 ×
((coe1‘𝐴)‘(𝑥 − 𝐷))), 0 ))) |