Step | Hyp | Ref
| Expression |
1 | | ply1mulgsum.p |
. . . . . . 7
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | ply1mulgsum.pm |
. . . . . . 7
⊢ × =
(.r‘𝑃) |
3 | | ply1mulgsum.rm |
. . . . . . 7
⊢ ∗ =
(.r‘𝑅) |
4 | | ply1mulgsum.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
5 | 1, 2, 3, 4 | coe1mul 19640 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (coe1‘(𝐾 × 𝐿)) = (𝑚 ∈ ℕ0 ↦ (𝑅 Σg
(𝑖 ∈ (0...𝑚) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))) |
6 | 5 | adantr 481 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
(coe1‘(𝐾
×
𝐿)) = (𝑚 ∈ ℕ0 ↦ (𝑅 Σg
(𝑖 ∈ (0...𝑚) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))) |
7 | 6 | fveq1d 6193 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝐾
×
𝐿))‘𝑛) = ((𝑚 ∈ ℕ0 ↦ (𝑅 Σg
(𝑖 ∈ (0...𝑚) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))‘𝑛)) |
8 | | eqidd 2623 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑚 ∈ ℕ0
↦ (𝑅
Σg (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖)))))) = (𝑚 ∈ ℕ0 ↦ (𝑅 Σg
(𝑖 ∈ (0...𝑚) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))) |
9 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (0...𝑚) = (0...𝑛)) |
10 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑚 − 𝑖) = (𝑛 − 𝑖)) |
11 | 10 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((coe1‘𝐿)‘(𝑚 − 𝑖)) = ((coe1‘𝐿)‘(𝑛 − 𝑖))) |
12 | 11 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))) = (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))) |
13 | 9, 12 | mpteq12dv 4733 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖)))) = (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖))))) |
14 | 13 | oveq2d 6666 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (𝑅 Σg (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))) = (𝑅 Σg (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))))) |
15 | 14 | adantl 482 |
. . . . 5
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑚 = 𝑛) → (𝑅 Σg (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))) = (𝑅 Σg (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))))) |
16 | | simpr 477 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
17 | | ovexd 6680 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑅 Σg
(𝑖 ∈ (0...𝑛) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖))))) ∈ V) |
18 | 8, 15, 16, 17 | fvmptd 6288 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ (𝑅
Σg (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))‘𝑛) = (𝑅 Σg (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))))) |
19 | | ply1mulgsum.x |
. . . . . 6
⊢ 𝑋 = (var1‘𝑅) |
20 | | ply1mulgsum.e |
. . . . . . 7
⊢ ↑ =
(.g‘𝑀) |
21 | | ply1mulgsum.m |
. . . . . . . 8
⊢ 𝑀 = (mulGrp‘𝑃) |
22 | 21 | fveq2i 6194 |
. . . . . . 7
⊢
(.g‘𝑀) = (.g‘(mulGrp‘𝑃)) |
23 | 20, 22 | eqtri 2644 |
. . . . . 6
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
24 | | simp1 1061 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑅 ∈ Ring) |
25 | 24 | adantr 481 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring) |
26 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
27 | | ply1mulgsum.sm |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑃) |
28 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
29 | | ringcmn 18581 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
30 | 29 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑅 ∈ CMnd) |
31 | 30 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑅 ∈
CMnd) |
32 | | fzfid 12772 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0...𝑘) ∈
Fin) |
33 | | simpll1 1100 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑅 ∈
Ring) |
34 | 33 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ Ring
∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑙 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
35 | | simp2 1062 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝐾 ∈ 𝐵) |
36 | 35 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐾 ∈ 𝐵) |
37 | | elfznn0 12433 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (0...𝑘) → 𝑙 ∈ ℕ0) |
38 | | ply1mulgsum.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (coe1‘𝐾) |
39 | 38, 4, 1, 26 | coe1fvalcl 19582 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑙 ∈ ℕ0) → (𝐴‘𝑙) ∈ (Base‘𝑅)) |
40 | 36, 37, 39 | syl2an 494 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ Ring
∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑙 ∈ (0...𝑘)) → (𝐴‘𝑙) ∈ (Base‘𝑅)) |
41 | | simp3 1063 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝐿 ∈ 𝐵) |
42 | 41 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐿 ∈ 𝐵) |
43 | | fznn0sub 12373 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (0...𝑘) → (𝑘 − 𝑙) ∈
ℕ0) |
44 | | ply1mulgsum.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (coe1‘𝐿) |
45 | 44, 4, 1, 26 | coe1fvalcl 19582 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ 𝐵 ∧ (𝑘 − 𝑙) ∈ ℕ0) → (𝐶‘(𝑘 − 𝑙)) ∈ (Base‘𝑅)) |
46 | 42, 43, 45 | syl2an 494 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ Ring
∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑙 ∈ (0...𝑘)) → (𝐶‘(𝑘 − 𝑙)) ∈ (Base‘𝑅)) |
47 | 26, 3 | ringcl 18561 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝐴‘𝑙) ∈ (Base‘𝑅) ∧ (𝐶‘(𝑘 − 𝑙)) ∈ (Base‘𝑅)) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
48 | 34, 40, 46, 47 | syl3anc 1326 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ Ring
∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑙 ∈ (0...𝑘)) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
49 | 48 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ∀𝑙 ∈
(0...𝑘)((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
50 | 26, 31, 32, 49 | gsummptcl 18366 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘𝑅)) |
51 | 50 | ralrimiva 2966 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 (𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘𝑅)) |
52 | 1, 4, 38, 44, 19, 2, 27, 3, 21, 20 | ply1mulgsumlem3 42176 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅)) |
53 | 52 | adantr 481 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅)) |
54 | 1, 4, 19, 23, 25, 26, 27, 28, 51, 53, 16 | gsummoncoe1 19674 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛) = ⦋𝑛 / 𝑘⦌(𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) |
55 | | vex 3203 |
. . . . . 6
⊢ 𝑛 ∈ V |
56 | | csbov2g 6691 |
. . . . . . 7
⊢ (𝑛 ∈ V →
⦋𝑛 / 𝑘⦌(𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) = (𝑅 Σg
⦋𝑛 / 𝑘⦌(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) |
57 | | id 22 |
. . . . . . . . 9
⊢ (𝑛 ∈ V → 𝑛 ∈ V) |
58 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → (0...𝑘) = (0...𝑛)) |
59 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝑘 − 𝑙) = (𝑛 − 𝑙)) |
60 | 59 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝐶‘(𝑘 − 𝑙)) = (𝐶‘(𝑛 − 𝑙))) |
61 | 60 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) = ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))) |
62 | 58, 61 | mpteq12dv 4733 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) |
63 | 62 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑛 ∈ V ∧ 𝑘 = 𝑛) → (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) |
64 | 57, 63 | csbied 3560 |
. . . . . . . 8
⊢ (𝑛 ∈ V →
⦋𝑛 / 𝑘⦌(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) |
65 | 64 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑛 ∈ V → (𝑅 Σg
⦋𝑛 / 𝑘⦌(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) = (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))))) |
66 | 56, 65 | eqtrd 2656 |
. . . . . 6
⊢ (𝑛 ∈ V →
⦋𝑛 / 𝑘⦌(𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) = (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))))) |
67 | 55, 66 | mp1i 13 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
⦋𝑛 / 𝑘⦌(𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) = (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))))) |
68 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑖 → (𝐴‘𝑙) = (𝐴‘𝑖)) |
69 | 38 | fveq1i 6192 |
. . . . . . . . . 10
⊢ (𝐴‘𝑖) = ((coe1‘𝐾)‘𝑖) |
70 | 68, 69 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑙 = 𝑖 → (𝐴‘𝑙) = ((coe1‘𝐾)‘𝑖)) |
71 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑖 → (𝑛 − 𝑙) = (𝑛 − 𝑖)) |
72 | 71 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑖 → (𝐶‘(𝑛 − 𝑙)) = (𝐶‘(𝑛 − 𝑖))) |
73 | 44 | fveq1i 6192 |
. . . . . . . . . 10
⊢ (𝐶‘(𝑛 − 𝑖)) = ((coe1‘𝐿)‘(𝑛 − 𝑖)) |
74 | 72, 73 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑙 = 𝑖 → (𝐶‘(𝑛 − 𝑙)) = ((coe1‘𝐿)‘(𝑛 − 𝑖))) |
75 | 70, 74 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑙 = 𝑖 → ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))) = (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))) |
76 | 75 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))) = (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))) |
77 | 76 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))) = (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖))))) |
78 | 77 | oveq2d 6666 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑅 Σg
(𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (𝑅 Σg (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))))) |
79 | 54, 67, 78 | 3eqtrrd 2661 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑅 Σg
(𝑖 ∈ (0...𝑛) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖))))) = ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛)) |
80 | 7, 18, 79 | 3eqtrd 2660 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝐾
×
𝐿))‘𝑛) =
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛)) |
81 | 80 | ralrimiva 2966 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∀𝑛 ∈ ℕ0
((coe1‘(𝐾
×
𝐿))‘𝑛) =
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛)) |
82 | 1 | ply1ring 19618 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
83 | 4, 2 | ringcl 18561 |
. . . 4
⊢ ((𝑃 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝐾 × 𝐿) ∈ 𝐵) |
84 | 82, 83 | syl3an1 1359 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝐾 × 𝐿) ∈ 𝐵) |
85 | | eqid 2622 |
. . . 4
⊢
(0g‘𝑃) = (0g‘𝑃) |
86 | | ringcmn 18581 |
. . . . . 6
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) |
87 | 82, 86 | syl 17 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑃 ∈ CMnd) |
88 | 87 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑃 ∈ CMnd) |
89 | | nn0ex 11298 |
. . . . 5
⊢
ℕ0 ∈ V |
90 | 89 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ℕ0 ∈
V) |
91 | 1 | ply1lmod 19622 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
92 | 91 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑃 ∈ LMod) |
93 | 92 | adantr 481 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod) |
94 | 30 | adantr 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ CMnd) |
95 | | fzfid 12772 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
96 | | simpll1 1100 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
97 | 35 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝐾 ∈ 𝐵) |
98 | 97, 37, 39 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → (𝐴‘𝑙) ∈ (Base‘𝑅)) |
99 | 41 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝐿 ∈ 𝐵) |
100 | 99, 43, 45 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → (𝐶‘(𝑘 − 𝑙)) ∈ (Base‘𝑅)) |
101 | 96, 98, 100, 47 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
102 | 101 | ralrimiva 2966 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
∀𝑙 ∈ (0...𝑘)((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
103 | 26, 94, 95, 102 | gsummptcl 18366 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘𝑅)) |
104 | 24 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
105 | 1 | ply1sca 19623 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
106 | 104, 105 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 = (Scalar‘𝑃)) |
107 | 106 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
108 | 103, 107 | eleqtrd 2703 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘(Scalar‘𝑃))) |
109 | 21 | ringmgp 18553 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd) |
110 | 82, 109 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
111 | 110 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑀 ∈ Mnd) |
112 | 111 | adantr 481 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈ Mnd) |
113 | | simpr 477 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
114 | 19, 1, 4 | vr1cl 19587 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
115 | 114 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
116 | 115 | adantr 481 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
117 | 21, 4 | mgpbas 18495 |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑀) |
118 | 117, 20 | mulgnn0cl 17558 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
119 | 112, 113,
116, 118 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
120 | | eqid 2622 |
. . . . . . 7
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
121 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
122 | 4, 120, 27, 121 | lmodvscl 18880 |
. . . . . 6
⊢ ((𝑃 ∈ LMod ∧ (𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)) ∈ 𝐵) |
123 | 93, 108, 119, 122 | syl3anc 1326 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)) ∈ 𝐵) |
124 | | eqid 2622 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) |
125 | 123, 124 | fmptd 6385 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))):ℕ0⟶𝐵) |
126 | 1, 4, 38, 44, 19, 2, 27, 3, 21, 20 | ply1mulgsumlem4 42177 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) |
127 | 4, 85, 88, 90, 125, 126 | gsumcl 18316 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))) ∈ 𝐵) |
128 | | eqid 2622 |
. . . 4
⊢
(coe1‘(𝐾 × 𝐿)) = (coe1‘(𝐾 × 𝐿)) |
129 | | eqid 2622 |
. . . 4
⊢
(coe1‘(𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))))) = (coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))))) |
130 | 1, 4, 128, 129 | ply1coe1eq 19668 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐾 × 𝐿) ∈ 𝐵 ∧ (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))) ∈ 𝐵) → (∀𝑛 ∈ ℕ0
((coe1‘(𝐾
×
𝐿))‘𝑛) =
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛) ↔ (𝐾 × 𝐿) = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))) |
131 | 24, 84, 127, 130 | syl3anc 1326 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∀𝑛 ∈ ℕ0
((coe1‘(𝐾
×
𝐿))‘𝑛) =
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛) ↔ (𝐾 × 𝐿) = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))) |
132 | 81, 131 | mpbid 222 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝐾 × 𝐿) = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))))) |