Proof of Theorem chpscmatgsummon
Step | Hyp | Ref
| Expression |
1 | | chp0mat.c |
. . 3
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
2 | | chp0mat.p |
. . 3
⊢ 𝑃 = (Poly1‘𝑅) |
3 | | chp0mat.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
4 | | chp0mat.x |
. . 3
⊢ 𝑋 = (var1‘𝑅) |
5 | | chp0mat.g |
. . 3
⊢ 𝐺 = (mulGrp‘𝑃) |
6 | | chp0mat.m |
. . 3
⊢ ↑ =
(.g‘𝐺) |
7 | | chpscmat.d |
. . 3
⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} |
8 | | chpscmat.s |
. . 3
⊢ 𝑆 = (algSc‘𝑃) |
9 | | chpscmat.m |
. . 3
⊢ − =
(-g‘𝑃) |
10 | | chpscmatgsum.f |
. . 3
⊢ 𝐹 = (.g‘𝑃) |
11 | | chpscmatgsum.h |
. . 3
⊢ 𝐻 = (mulGrp‘𝑅) |
12 | | chpscmatgsum.e |
. . 3
⊢ 𝐸 = (.g‘𝐻) |
13 | | chpscmatgsum.i |
. . 3
⊢ 𝐼 = (invg‘𝑅) |
14 | | chpscmatgsum.s |
. . 3
⊢ · = (
·𝑠 ‘𝑃) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | chpscmatgsumbin 22193 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐶‘𝑀) = (𝑃 Σg (𝑙 ∈
(0...(♯‘𝑁))
↦ (((♯‘𝑁)C𝑙)𝐹((((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) · (𝑙 ↑ 𝑋)))))) |
16 | | crngring 19976 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
17 | 16 | adantl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring) |
18 | 2 | ply1lmod 21623 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ LMod) |
20 | 19 | ad2antrr 724 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → 𝑃 ∈ LMod) |
21 | | eqid 2736 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
22 | 11, 21 | mgpbas 19902 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝐻) |
23 | 11 | ringmgp 19970 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝐻 ∈ Mnd) |
24 | 17, 23 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐻 ∈ Mnd) |
25 | 24 | ad2antrr 724 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → 𝐻 ∈ Mnd) |
26 | | fznn0sub 13473 |
. . . . . . . . 9
⊢ (𝑙 ∈
(0...(♯‘𝑁))
→ ((♯‘𝑁)
− 𝑙) ∈
ℕ0) |
27 | 26 | adantl 482 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → ((♯‘𝑁) − 𝑙) ∈
ℕ0) |
28 | | ringgrp 19969 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
29 | 16, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Grp) |
30 | 29 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Grp) |
31 | | simp2 1137 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽)) → 𝐽 ∈ 𝑁) |
32 | | elrabi 3639 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} → 𝑀 ∈ (Base‘𝐴)) |
33 | 32, 7 | eleq2s 2856 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ 𝐷 → 𝑀 ∈ (Base‘𝐴)) |
34 | 33 | 3ad2ant1 1133 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽)) → 𝑀 ∈ (Base‘𝐴)) |
35 | 31, 31, 34 | 3jca 1128 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽)) → (𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) |
36 | 35 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) |
37 | 3, 21 | matecl 21774 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐽𝑀𝐽) ∈ (Base‘𝑅)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐽𝑀𝐽) ∈ (Base‘𝑅)) |
39 | 21, 13 | grpinvcl 18798 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ (𝐽𝑀𝐽) ∈ (Base‘𝑅)) → (𝐼‘(𝐽𝑀𝐽)) ∈ (Base‘𝑅)) |
40 | 30, 38, 39 | syl2an2r 683 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐼‘(𝐽𝑀𝐽)) ∈ (Base‘𝑅)) |
41 | 40 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → (𝐼‘(𝐽𝑀𝐽)) ∈ (Base‘𝑅)) |
42 | 22, 12, 25, 27, 41 | mulgnn0cld 18897 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → (((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) ∈ (Base‘𝑅)) |
43 | 2 | ply1sca 21624 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃)) |
44 | 43 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝑃)) |
45 | 44 | eqcomd 2742 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(Scalar‘𝑃) = 𝑅) |
46 | 45 | fveq2d 6846 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(Base‘(Scalar‘𝑃)) = (Base‘𝑅)) |
47 | 46 | ad2antrr 724 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅)) |
48 | 42, 47 | eleqtrrd 2841 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → (((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) ∈ (Base‘(Scalar‘𝑃))) |
49 | | hashcl 14256 |
. . . . . . . 8
⊢ (𝑁 ∈ Fin →
(♯‘𝑁) ∈
ℕ0) |
50 | 49 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (♯‘𝑁) ∈
ℕ0) |
51 | | elfzelz 13441 |
. . . . . . 7
⊢ (𝑙 ∈
(0...(♯‘𝑁))
→ 𝑙 ∈
ℤ) |
52 | | bccl 14222 |
. . . . . . 7
⊢
(((♯‘𝑁)
∈ ℕ0 ∧ 𝑙 ∈ ℤ) → ((♯‘𝑁)C𝑙) ∈
ℕ0) |
53 | 50, 51, 52 | syl2an 596 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → ((♯‘𝑁)C𝑙) ∈
ℕ0) |
54 | | eqid 2736 |
. . . . . . . 8
⊢
(Base‘𝑃) =
(Base‘𝑃) |
55 | 5, 54 | mgpbas 19902 |
. . . . . . 7
⊢
(Base‘𝑃) =
(Base‘𝐺) |
56 | 2 | ply1ring 21619 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
57 | 5 | ringmgp 19970 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring → 𝐺 ∈ Mnd) |
58 | 16, 56, 57 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝐺 ∈ Mnd) |
59 | 58 | adantl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐺 ∈ Mnd) |
60 | 59 | ad2antrr 724 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → 𝐺 ∈ Mnd) |
61 | | elfznn0 13534 |
. . . . . . . 8
⊢ (𝑙 ∈
(0...(♯‘𝑁))
→ 𝑙 ∈
ℕ0) |
62 | 61 | adantl 482 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → 𝑙 ∈ ℕ0) |
63 | 4, 2, 54 | vr1cl 21588 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
64 | 17, 63 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑋 ∈ (Base‘𝑃)) |
65 | 64 | ad2antrr 724 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → 𝑋 ∈ (Base‘𝑃)) |
66 | 55, 6, 60, 62, 65 | mulgnn0cld 18897 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → (𝑙 ↑ 𝑋) ∈ (Base‘𝑃)) |
67 | | eqid 2736 |
. . . . . . 7
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
68 | | eqid 2736 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
69 | | eqid 2736 |
. . . . . . 7
⊢
(.g‘(Scalar‘𝑃)) =
(.g‘(Scalar‘𝑃)) |
70 | 54, 67, 14, 68, 10, 69 | lmodvsmmulgdi 20357 |
. . . . . 6
⊢ ((𝑃 ∈ LMod ∧
((((♯‘𝑁)
− 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) ∈ (Base‘(Scalar‘𝑃)) ∧ ((♯‘𝑁)C𝑙) ∈ ℕ0 ∧ (𝑙 ↑ 𝑋) ∈ (Base‘𝑃))) → (((♯‘𝑁)C𝑙)𝐹((((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) · (𝑙 ↑ 𝑋))) = ((((♯‘𝑁)C𝑙)(.g‘(Scalar‘𝑃))(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋))) |
71 | 20, 48, 53, 66, 70 | syl13anc 1372 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → (((♯‘𝑁)C𝑙)𝐹((((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) · (𝑙 ↑ 𝑋))) = ((((♯‘𝑁)C𝑙)(.g‘(Scalar‘𝑃))(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋))) |
72 | | chpscmatgsum.z |
. . . . . . . . 9
⊢ 𝑍 = (.g‘𝑅) |
73 | 44 | fveq2d 6846 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(.g‘𝑅) =
(.g‘(Scalar‘𝑃))) |
74 | 72, 73 | eqtr2id 2789 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(.g‘(Scalar‘𝑃)) = 𝑍) |
75 | 74 | ad2antrr 724 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) →
(.g‘(Scalar‘𝑃)) = 𝑍) |
76 | 75 | oveqd 7374 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → (((♯‘𝑁)C𝑙)(.g‘(Scalar‘𝑃))(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) = (((♯‘𝑁)C𝑙)𝑍(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))))) |
77 | 76 | oveq1d 7372 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → ((((♯‘𝑁)C𝑙)(.g‘(Scalar‘𝑃))(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋)) = ((((♯‘𝑁)C𝑙)𝑍(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋))) |
78 | 71, 77 | eqtrd 2776 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) ∧ 𝑙 ∈ (0...(♯‘𝑁))) → (((♯‘𝑁)C𝑙)𝐹((((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) · (𝑙 ↑ 𝑋))) = ((((♯‘𝑁)C𝑙)𝑍(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋))) |
79 | 78 | mpteq2dva 5205 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝑙 ∈ (0...(♯‘𝑁)) ↦ (((♯‘𝑁)C𝑙)𝐹((((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) · (𝑙 ↑ 𝑋)))) = (𝑙 ∈ (0...(♯‘𝑁)) ↦ ((((♯‘𝑁)C𝑙)𝑍(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋)))) |
80 | 79 | oveq2d 7373 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝑃 Σg (𝑙 ∈
(0...(♯‘𝑁))
↦ (((♯‘𝑁)C𝑙)𝐹((((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) · (𝑙 ↑ 𝑋))))) = (𝑃 Σg (𝑙 ∈
(0...(♯‘𝑁))
↦ ((((♯‘𝑁)C𝑙)𝑍(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋))))) |
81 | 15, 80 | eqtrd 2776 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐶‘𝑀) = (𝑃 Σg (𝑙 ∈
(0...(♯‘𝑁))
↦ ((((♯‘𝑁)C𝑙)𝑍(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋))))) |