Metamath Proof Explorer

Theorem chpscmatgsumbin

Description: The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of binomials. (Contributed by AV, 2-Sep-2019)

Ref Expression
Hypotheses chp0mat.c 
|- C = ( N CharPlyMat R )
chp0mat.p 
|- P = ( Poly1 ` R )
chp0mat.a 
|- A = ( N Mat R )
chp0mat.x 
|- X = ( var1 ` R )
chp0mat.g 
|- G = ( mulGrp ` P )
chp0mat.m 
|- .^ = ( .g ` G )
chpscmat.d 
|- D = { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) }
chpscmat.s 
|- S = ( algSc ` P )
chpscmat.m 
|- .- = ( -g ` P )
chpscmatgsum.f 
|- F = ( .g ` P )
chpscmatgsum.h 
|- H = ( mulGrp ` R )
chpscmatgsum.e 
|- E = ( .g ` H )
chpscmatgsum.i 
|- I = ( invg ` R )
chpscmatgsum.s 
|- .x. = ( .s ` P )
Assertion chpscmatgsumbin 
|- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( C ` M ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chp0mat.c 
 |-  C = ( N CharPlyMat R )
2 chp0mat.p 
 |-  P = ( Poly1 ` R )
3 chp0mat.a 
 |-  A = ( N Mat R )
4 chp0mat.x 
 |-  X = ( var1 ` R )
5 chp0mat.g 
 |-  G = ( mulGrp ` P )
6 chp0mat.m 
 |-  .^ = ( .g ` G )
7 chpscmat.d 
 |-  D = { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) }
8 chpscmat.s 
 |-  S = ( algSc ` P )
9 chpscmat.m 
 |-  .- = ( -g ` P )
10 chpscmatgsum.f 
 |-  F = ( .g ` P )
11 chpscmatgsum.h 
 |-  H = ( mulGrp ` R )
12 chpscmatgsum.e 
 |-  E = ( .g ` H )
13 chpscmatgsum.i 
 |-  I = ( invg ` R )
14 chpscmatgsum.s 
 |-  .x. = ( .s ` P )
15 1 2 3 4 5 6 7 8 9 chpscmat0 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( C ` M ) = ( ( # ` N ) .^ ( X .- ( S ` ( J M J ) ) ) ) )
16 crngring 
 |-  ( R e. CRing -> R e. Ring )
17 16 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
18 eqid 
 |-  ( Base ` P ) = ( Base ` P )
19 4 2 18 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
20 17 19 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` P ) )
21 20 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> X e. ( Base ` P ) )
22 16 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> R e. Ring )
23 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
24 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
25 2 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
26 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
27 8 23 24 25 26 18 asclf 
 |-  ( R e. Ring -> S : ( Base ` ( Scalar ` P ) ) --> ( Base ` P ) )
28 22 27 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> S : ( Base ` ( Scalar ` P ) ) --> ( Base ` P ) )
29 simpr2 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> J e. N )
30 elrabi 
 |-  ( M e. { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) } -> M e. ( Base ` A ) )
31 30 a1d 
 |-  ( M e. { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) } -> ( ( N e. Fin /\ R e. CRing ) -> M e. ( Base ` A ) ) )
32 31 7 eleq2s 
 |-  ( M e. D -> ( ( N e. Fin /\ R e. CRing ) -> M e. ( Base ` A ) ) )
33 32 3ad2ant1 
 |-  ( ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) -> ( ( N e. Fin /\ R e. CRing ) -> M e. ( Base ` A ) ) )
34 33 impcom 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> M e. ( Base ` A ) )
35 eqid 
 |-  ( Base ` R ) = ( Base ` R )
36 3 35 matecl 
 |-  ( ( J e. N /\ J e. N /\ M e. ( Base ` A ) ) -> ( J M J ) e. ( Base ` R ) )
37 29 29 34 36 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( J M J ) e. ( Base ` R ) )
38 2 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
39 38 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` P ) )
40 39 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Scalar ` P ) = R )
41 40 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( Scalar ` P ) = R )
42 41 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
43 37 42 eleqtrrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( J M J ) e. ( Base ` ( Scalar ` P ) ) )
44 28 43 ffvelrnd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( S ` ( J M J ) ) e. ( Base ` P ) )
45 eqid 
 |-  ( +g ` P ) = ( +g ` P )
46 eqid 
 |-  ( invg ` P ) = ( invg ` P )
47 18 45 46 9 grpsubval 
 |-  ( ( X e. ( Base ` P ) /\ ( S ` ( J M J ) ) e. ( Base ` P ) ) -> ( X .- ( S ` ( J M J ) ) ) = ( X ( +g ` P ) ( ( invg ` P ) ` ( S ` ( J M J ) ) ) ) )
48 21 44 47 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( X .- ( S ` ( J M J ) ) ) = ( X ( +g ` P ) ( ( invg ` P ) ` ( S ` ( J M J ) ) ) ) )
49 17 25 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. LMod )
50 49 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> P e. LMod )
51 17 24 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. Ring )
52 51 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> P e. Ring )
53 eqid 
 |-  ( invg ` ( Scalar ` P ) ) = ( invg ` ( Scalar ` P ) )
54 8 23 26 53 46 asclinvg 
 |-  ( ( P e. LMod /\ P e. Ring /\ ( J M J ) e. ( Base ` ( Scalar ` P ) ) ) -> ( ( invg ` P ) ` ( S ` ( J M J ) ) ) = ( S ` ( ( invg ` ( Scalar ` P ) ) ` ( J M J ) ) ) )
55 50 52 43 54 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( ( invg ` P ) ` ( S ` ( J M J ) ) ) = ( S ` ( ( invg ` ( Scalar ` P ) ) ` ( J M J ) ) ) )
56 39 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( invg ` R ) = ( invg ` ( Scalar ` P ) ) )
57 56 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( invg ` R ) = ( invg ` ( Scalar ` P ) ) )
58 13 57 eqtr2id 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( invg ` ( Scalar ` P ) ) = I )
59 58 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( ( invg ` ( Scalar ` P ) ) ` ( J M J ) ) = ( I ` ( J M J ) ) )
60 59 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( S ` ( ( invg ` ( Scalar ` P ) ) ` ( J M J ) ) ) = ( S ` ( I ` ( J M J ) ) ) )
61 55 60 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( ( invg ` P ) ` ( S ` ( J M J ) ) ) = ( S ` ( I ` ( J M J ) ) ) )
62 61 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( X ( +g ` P ) ( ( invg ` P ) ` ( S ` ( J M J ) ) ) ) = ( X ( +g ` P ) ( S ` ( I ` ( J M J ) ) ) ) )
63 48 62 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( X .- ( S ` ( J M J ) ) ) = ( X ( +g ` P ) ( S ` ( I ` ( J M J ) ) ) ) )
64 63 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( ( # ` N ) .^ ( X .- ( S ` ( J M J ) ) ) ) = ( ( # ` N ) .^ ( X ( +g ` P ) ( S ` ( I ` ( J M J ) ) ) ) ) )
65 simplr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> R e. CRing )
66 hashcl 
 |-  ( N e. Fin -> ( # ` N ) e. NN0 )
67 66 ad2antrr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( # ` N ) e. NN0 )
68 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
69 16 68 syl 
 |-  ( R e. CRing -> R e. Grp )
70 69 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> R e. Grp )
71 35 13 grpinvcl 
 |-  ( ( R e. Grp /\ ( J M J ) e. ( Base ` R ) ) -> ( I ` ( J M J ) ) e. ( Base ` R ) )
72 70 37 71 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( I ` ( J M J ) ) e. ( Base ` R ) )
73 eqid 
 |-  ( .r ` P ) = ( .r ` P )
74 2 4 45 73 10 5 6 35 8 11 12 lply1binomsc 
 |-  ( ( R e. CRing /\ ( # ` N ) e. NN0 /\ ( I ` ( J M J ) ) e. ( Base ` R ) ) -> ( ( # ` N ) .^ ( X ( +g ` P ) ( S ` ( I ` ( J M J ) ) ) ) ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( S ` ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) ( .r ` P ) ( l .^ X ) ) ) ) ) )
75 65 67 72 74 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( ( # ` N ) .^ ( X ( +g ` P ) ( S ` ( I ` ( J M J ) ) ) ) ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( S ` ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) ( .r ` P ) ( l .^ X ) ) ) ) ) )
76 2 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
77 76 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. AssAlg )
78 77 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> P e. AssAlg )
79 11 ringmgp 
 |-  ( R e. Ring -> H e. Mnd )
80 17 79 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> H e. Mnd )
81 80 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> H e. Mnd )
82 fznn0sub 
 |-  ( l e. ( 0 ... ( # ` N ) ) -> ( ( # ` N ) - l ) e. NN0 )
83 82 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( # ` N ) - l ) e. NN0 )
84 11 35 mgpbas 
 |-  ( Base ` R ) = ( Base ` H )
85 72 84 eleqtrdi 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( I ` ( J M J ) ) e. ( Base ` H ) )
86 85 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( I ` ( J M J ) ) e. ( Base ` H ) )
87 eqid 
 |-  ( Base ` H ) = ( Base ` H )
88 87 12 mulgnn0cl 
 |-  ( ( H e. Mnd /\ ( ( # ` N ) - l ) e. NN0 /\ ( I ` ( J M J ) ) e. ( Base ` H ) ) -> ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) e. ( Base ` H ) )
89 81 83 86 88 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) e. ( Base ` H ) )
90 40 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
91 90 84 eqtrdi 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` H ) )
92 91 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` H ) )
93 89 92 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) e. ( Base ` ( Scalar ` P ) ) )
94 5 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
95 16 24 94 3syl 
 |-  ( R e. CRing -> G e. Mnd )
96 95 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ l e. ( 0 ... ( # ` N ) ) ) -> G e. Mnd )
97 elfznn0 
 |-  ( l e. ( 0 ... ( # ` N ) ) -> l e. NN0 )
98 97 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ l e. ( 0 ... ( # ` N ) ) ) -> l e. NN0 )
99 20 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ l e. ( 0 ... ( # ` N ) ) ) -> X e. ( Base ` P ) )
100 5 18 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
101 100 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ l e. NN0 /\ X e. ( Base ` P ) ) -> ( l .^ X ) e. ( Base ` P ) )
102 96 98 99 101 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( l .^ X ) e. ( Base ` P ) )
103 102 adantlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( l .^ X ) e. ( Base ` P ) )
104 8 23 26 18 73 14 asclmul1 
 |-  ( ( P e. AssAlg /\ ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) e. ( Base ` ( Scalar ` P ) ) /\ ( l .^ X ) e. ( Base ` P ) ) -> ( ( S ` ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) ( .r ` P ) ( l .^ X ) ) = ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) )
105 78 93 103 104 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( S ` ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) ( .r ` P ) ( l .^ X ) ) = ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) )
106 105 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( # ` N ) _C l ) F ( ( S ` ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) ( .r ` P ) ( l .^ X ) ) ) = ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) )
107 106 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( S ` ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) ( .r ` P ) ( l .^ X ) ) ) ) = ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) ) )
108 107 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( S ` ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) ( .r ` P ) ( l .^ X ) ) ) ) ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) ) ) )
109 75 108 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( ( # ` N ) .^ ( X ( +g ` P ) ( S ` ( I ` ( J M J ) ) ) ) ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) ) ) )
110 15 64 109 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( C ` M ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) ) ) )