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 21038 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (coe1‘(𝐾 × 𝐿)) = (𝑚 ∈ ℕ0 ↦ (𝑅 Σg
(𝑖 ∈ (0...𝑚) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))) |
6 | 5 | adantr 484 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
(coe1‘(𝐾
×
𝐿)) = (𝑚 ∈ ℕ0 ↦ (𝑅 Σg
(𝑖 ∈ (0...𝑚) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))) |
7 | 6 | fveq1d 6670 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝐾
×
𝐿))‘𝑛) = ((𝑚 ∈ ℕ0 ↦ (𝑅 Σg
(𝑖 ∈ (0...𝑚) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))‘𝑛)) |
8 | | eqidd 2739 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑚 ∈ ℕ0
↦ (𝑅
Σg (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖)))))) = (𝑚 ∈ ℕ0 ↦ (𝑅 Σg
(𝑖 ∈ (0...𝑚) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))) |
9 | | oveq2 7172 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (0...𝑚) = (0...𝑛)) |
10 | | fvoveq1 7187 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((coe1‘𝐿)‘(𝑚 − 𝑖)) = ((coe1‘𝐿)‘(𝑛 − 𝑖))) |
11 | 10 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))) = (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))) |
12 | 9, 11 | mpteq12dv 5112 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖)))) = (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖))))) |
13 | 12 | oveq2d 7180 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (𝑅 Σg (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))) = (𝑅 Σg (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))))) |
14 | 13 | adantl 485 |
. . . . 5
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑚 = 𝑛) → (𝑅 Σg (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))) = (𝑅 Σg (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))))) |
15 | | simpr 488 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
16 | | ovexd 7199 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑅 Σg
(𝑖 ∈ (0...𝑛) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖))))) ∈ V) |
17 | 8, 14, 15, 16 | fvmptd 6776 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ (𝑅
Σg (𝑖 ∈ (0...𝑚) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑚 − 𝑖))))))‘𝑛) = (𝑅 Σg (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))))) |
18 | | ply1mulgsum.x |
. . . . . 6
⊢ 𝑋 = (var1‘𝑅) |
19 | | ply1mulgsum.e |
. . . . . . 7
⊢ ↑ =
(.g‘𝑀) |
20 | | ply1mulgsum.m |
. . . . . . . 8
⊢ 𝑀 = (mulGrp‘𝑃) |
21 | 20 | fveq2i 6671 |
. . . . . . 7
⊢
(.g‘𝑀) = (.g‘(mulGrp‘𝑃)) |
22 | 19, 21 | eqtri 2761 |
. . . . . 6
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
23 | | simp1 1137 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑅 ∈ Ring) |
24 | 23 | adantr 484 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring) |
25 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
26 | | ply1mulgsum.sm |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑃) |
27 | | eqid 2738 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
28 | | ringcmn 19446 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
29 | 28 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑅 ∈ CMnd) |
30 | 29 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑅 ∈
CMnd) |
31 | | fzfid 13425 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0...𝑘) ∈
Fin) |
32 | | simpll1 1213 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑅 ∈
Ring) |
33 | 32 | adantr 484 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ Ring
∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑙 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
34 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝐾 ∈ 𝐵) |
35 | 34 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐾 ∈ 𝐵) |
36 | | elfznn0 13084 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (0...𝑘) → 𝑙 ∈ ℕ0) |
37 | | ply1mulgsum.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (coe1‘𝐾) |
38 | 37, 4, 1, 25 | coe1fvalcl 20980 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑙 ∈ ℕ0) → (𝐴‘𝑙) ∈ (Base‘𝑅)) |
39 | 35, 36, 38 | syl2an 599 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ Ring
∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑙 ∈ (0...𝑘)) → (𝐴‘𝑙) ∈ (Base‘𝑅)) |
40 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝐿 ∈ 𝐵) |
41 | 40 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐿 ∈ 𝐵) |
42 | | fznn0sub 13023 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (0...𝑘) → (𝑘 − 𝑙) ∈
ℕ0) |
43 | | ply1mulgsum.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (coe1‘𝐿) |
44 | 43, 4, 1, 25 | coe1fvalcl 20980 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ 𝐵 ∧ (𝑘 − 𝑙) ∈ ℕ0) → (𝐶‘(𝑘 − 𝑙)) ∈ (Base‘𝑅)) |
45 | 41, 42, 44 | syl2an 599 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ Ring
∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑙 ∈ (0...𝑘)) → (𝐶‘(𝑘 − 𝑙)) ∈ (Base‘𝑅)) |
46 | 25, 3 | ringcl 19426 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝐴‘𝑙) ∈ (Base‘𝑅) ∧ (𝐶‘(𝑘 − 𝑙)) ∈ (Base‘𝑅)) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
47 | 33, 39, 45, 46 | syl3anc 1372 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ Ring
∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑙 ∈ (0...𝑘)) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
48 | 47 | ralrimiva 3096 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ∀𝑙 ∈
(0...𝑘)((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
49 | 25, 30, 31, 48 | gsummptcl 19199 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘𝑅)) |
50 | 49 | ralrimiva 3096 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 (𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘𝑅)) |
51 | 1, 4, 37, 43, 18, 2, 26, 3, 20, 19 | ply1mulgsumlem3 45247 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅)) |
52 | 51 | adantr 484 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅)) |
53 | 1, 4, 18, 22, 24, 25, 26, 27, 50, 52, 15 | gsummoncoe1 21072 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛) = ⦋𝑛 / 𝑘⦌(𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) |
54 | | vex 3401 |
. . . . . 6
⊢ 𝑛 ∈ V |
55 | | csbov2g 7210 |
. . . . . . 7
⊢ (𝑛 ∈ V →
⦋𝑛 / 𝑘⦌(𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) = (𝑅 Σg
⦋𝑛 / 𝑘⦌(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) |
56 | | id 22 |
. . . . . . . . 9
⊢ (𝑛 ∈ V → 𝑛 ∈ V) |
57 | | oveq2 7172 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → (0...𝑘) = (0...𝑛)) |
58 | | fvoveq1 7187 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝐶‘(𝑘 − 𝑙)) = (𝐶‘(𝑛 − 𝑙))) |
59 | 58 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) = ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))) |
60 | 57, 59 | mpteq12dv 5112 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) |
61 | 60 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑛 ∈ V ∧ 𝑘 = 𝑛) → (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) |
62 | 56, 61 | csbied 3824 |
. . . . . . . 8
⊢ (𝑛 ∈ V →
⦋𝑛 / 𝑘⦌(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) |
63 | 62 | oveq2d 7180 |
. . . . . . 7
⊢ (𝑛 ∈ V → (𝑅 Σg
⦋𝑛 / 𝑘⦌(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) = (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))))) |
64 | 55, 63 | eqtrd 2773 |
. . . . . 6
⊢ (𝑛 ∈ V →
⦋𝑛 / 𝑘⦌(𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) = (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))))) |
65 | 54, 64 | mp1i 13 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
⦋𝑛 / 𝑘⦌(𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) = (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))))) |
66 | | fveq2 6668 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑖 → (𝐴‘𝑙) = (𝐴‘𝑖)) |
67 | 37 | fveq1i 6669 |
. . . . . . . . . 10
⊢ (𝐴‘𝑖) = ((coe1‘𝐾)‘𝑖) |
68 | 66, 67 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝑙 = 𝑖 → (𝐴‘𝑙) = ((coe1‘𝐾)‘𝑖)) |
69 | | oveq2 7172 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑖 → (𝑛 − 𝑙) = (𝑛 − 𝑖)) |
70 | 69 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑖 → (𝐶‘(𝑛 − 𝑙)) = (𝐶‘(𝑛 − 𝑖))) |
71 | 43 | fveq1i 6669 |
. . . . . . . . . 10
⊢ (𝐶‘(𝑛 − 𝑖)) = ((coe1‘𝐿)‘(𝑛 − 𝑖)) |
72 | 70, 71 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝑙 = 𝑖 → (𝐶‘(𝑛 − 𝑙)) = ((coe1‘𝐿)‘(𝑛 − 𝑖))) |
73 | 68, 72 | oveq12d 7182 |
. . . . . . . 8
⊢ (𝑙 = 𝑖 → ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))) = (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))) |
74 | 73 | cbvmptv 5130 |
. . . . . . 7
⊢ (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))) = (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))) |
75 | 74 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙)))) = (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖))))) |
76 | 75 | oveq2d 7180 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑅 Σg
(𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (𝑅 Σg (𝑖 ∈ (0...𝑛) ↦ (((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖)))))) |
77 | 53, 65, 76 | 3eqtrrd 2778 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑅 Σg
(𝑖 ∈ (0...𝑛) ↦
(((coe1‘𝐾)‘𝑖) ∗
((coe1‘𝐿)‘(𝑛 − 𝑖))))) = ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛)) |
78 | 7, 17, 77 | 3eqtrd 2777 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝐾
×
𝐿))‘𝑛) =
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛)) |
79 | 78 | ralrimiva 3096 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∀𝑛 ∈ ℕ0
((coe1‘(𝐾
×
𝐿))‘𝑛) =
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛)) |
80 | 1 | ply1ring 21016 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
81 | 4, 2 | ringcl 19426 |
. . . 4
⊢ ((𝑃 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝐾 × 𝐿) ∈ 𝐵) |
82 | 80, 81 | syl3an1 1164 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝐾 × 𝐿) ∈ 𝐵) |
83 | | eqid 2738 |
. . . 4
⊢
(0g‘𝑃) = (0g‘𝑃) |
84 | | ringcmn 19446 |
. . . . . 6
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) |
85 | 80, 84 | syl 17 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑃 ∈ CMnd) |
86 | 85 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑃 ∈ CMnd) |
87 | | nn0ex 11975 |
. . . . 5
⊢
ℕ0 ∈ V |
88 | 87 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ℕ0 ∈
V) |
89 | 1 | ply1lmod 21020 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
90 | 89 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑃 ∈ LMod) |
91 | 90 | adantr 484 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod) |
92 | 29 | adantr 484 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ CMnd) |
93 | | fzfid 13425 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
94 | | simpll1 1213 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
95 | 34 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝐾 ∈ 𝐵) |
96 | 95, 36, 38 | syl2an 599 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → (𝐴‘𝑙) ∈ (Base‘𝑅)) |
97 | 40 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝐿 ∈ 𝐵) |
98 | 97, 42, 44 | syl2an 599 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → (𝐶‘(𝑘 − 𝑙)) ∈ (Base‘𝑅)) |
99 | 94, 96, 98, 46 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
100 | 99 | ralrimiva 3096 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
∀𝑙 ∈ (0...𝑘)((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))) ∈ (Base‘𝑅)) |
101 | 25, 92, 93, 100 | gsummptcl 19199 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘𝑅)) |
102 | 23 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
103 | 1 | ply1sca 21021 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
104 | 102, 103 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 = (Scalar‘𝑃)) |
105 | 104 | fveq2d 6672 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
106 | 101, 105 | eleqtrd 2835 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘(Scalar‘𝑃))) |
107 | 20 | ringmgp 19415 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd) |
108 | 80, 107 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
109 | 108 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑀 ∈ Mnd) |
110 | 109 | adantr 484 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈ Mnd) |
111 | | simpr 488 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
112 | 18, 1, 4 | vr1cl 20985 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
113 | 112 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
114 | 113 | adantr 484 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
115 | 20, 4 | mgpbas 19357 |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑀) |
116 | 115, 19 | mulgnn0cl 18355 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
117 | 110, 111,
114, 116 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
118 | | eqid 2738 |
. . . . . . 7
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
119 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
120 | 4, 118, 26, 119 | lmodvscl 19763 |
. . . . . 6
⊢ ((𝑃 ∈ LMod ∧ (𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)) ∈ 𝐵) |
121 | 91, 106, 117, 120 | syl3anc 1372 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)) ∈ 𝐵) |
122 | 121 | fmpttd 6883 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))):ℕ0⟶𝐵) |
123 | 1, 4, 37, 43, 18, 2, 26, 3, 20, 19 | ply1mulgsumlem4 45248 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) |
124 | 4, 83, 86, 88, 122, 123 | gsumcl 19147 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))) ∈ 𝐵) |
125 | | eqid 2738 |
. . . 4
⊢
(coe1‘(𝐾 × 𝐿)) = (coe1‘(𝐾 × 𝐿)) |
126 | | eqid 2738 |
. . . 4
⊢
(coe1‘(𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))))) = (coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))))) |
127 | 1, 4, 125, 126 | ply1coe1eq 21066 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐾 × 𝐿) ∈ 𝐵 ∧ (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))) ∈ 𝐵) → (∀𝑛 ∈ ℕ0
((coe1‘(𝐾
×
𝐿))‘𝑛) =
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛) ↔ (𝐾 × 𝐿) = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))) |
128 | 23, 82, 124, 127 | syl3anc 1372 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∀𝑛 ∈ ℕ0
((coe1‘(𝐾
×
𝐿))‘𝑛) =
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg
(𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))‘𝑛) ↔ (𝐾 × 𝐿) = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))) |
129 | 79, 128 | mpbid 235 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝐾 × 𝐿) = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑅
Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))))) |