Metamath Proof Explorer

Theorem mdetleib2

Description: Leibniz' formula can also be expanded by rows. (Contributed by Stefan O'Rear, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses mdetfval.d 
|- D = ( N maDet R )
mdetfval.a 
|- A = ( N Mat R )
mdetfval.b 
|- B = ( Base ` A )
mdetfval.p 
|- P = ( Base ` ( SymGrp ` N ) )
mdetfval.y 
|- Y = ( ZRHom ` R )
mdetfval.s 
|- S = ( pmSgn ` N )
mdetfval.t 
|- .x. = ( .r ` R )
mdetfval.u 
|- U = ( mulGrp ` R )
Assertion mdetleib2 
|- ( ( R e. CRing /\ M e. B ) -> ( D ` M ) = ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetfval.d 
 |-  D = ( N maDet R )
2 mdetfval.a 
 |-  A = ( N Mat R )
3 mdetfval.b 
 |-  B = ( Base ` A )
4 mdetfval.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
5 mdetfval.y 
 |-  Y = ( ZRHom ` R )
6 mdetfval.s 
 |-  S = ( pmSgn ` N )
7 mdetfval.t 
 |-  .x. = ( .r ` R )
8 mdetfval.u 
 |-  U = ( mulGrp ` R )
9 1 2 3 4 5 6 7 8 mdetleib 
 |-  ( M e. B -> ( D ` M ) = ( R gsum ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) ) )
10 9 adantl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( D ` M ) = ( R gsum ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) ) )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 crngring 
 |-  ( R e. CRing -> R e. Ring )
13 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
14 12 13 syl 
 |-  ( R e. CRing -> R e. CMnd )
15 14 adantr 
 |-  ( ( R e. CRing /\ M e. B ) -> R e. CMnd )
16 2 3 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
17 16 adantl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. _V ) )
18 17 simpld 
 |-  ( ( R e. CRing /\ M e. B ) -> N e. Fin )
19 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
20 19 4 symgbasfi 
 |-  ( N e. Fin -> P e. Fin )
21 18 20 syl 
 |-  ( ( R e. CRing /\ M e. B ) -> P e. Fin )
22 12 ad2antrr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> R e. Ring )
23 5 6 coeq12i 
 |-  ( Y o. S ) = ( ( ZRHom ` R ) o. ( pmSgn ` N ) )
24 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
25 23 24 eqeltrid 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( Y o. S ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
26 12 18 25 syl2an2r 
 |-  ( ( R e. CRing /\ M e. B ) -> ( Y o. S ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
27 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
28 27 11 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
29 4 28 mhmf 
 |-  ( ( Y o. S ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( Y o. S ) : P --> ( Base ` R ) )
30 26 29 syl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( Y o. S ) : P --> ( Base ` R ) )
31 30 ffvelrnda 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> ( ( Y o. S ) ` q ) e. ( Base ` R ) )
32 8 11 mgpbas 
 |-  ( Base ` R ) = ( Base ` U )
33 8 crngmgp 
 |-  ( R e. CRing -> U e. CMnd )
34 33 ad2antrr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> U e. CMnd )
35 18 adantr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> N e. Fin )
36 simpr 
 |-  ( ( R e. CRing /\ M e. B ) -> M e. B )
37 2 11 3 matbas2i 
 |-  ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
38 elmapi 
 |-  ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
39 36 37 38 3syl 
 |-  ( ( R e. CRing /\ M e. B ) -> M : ( N X. N ) --> ( Base ` R ) )
40 39 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) /\ y e. N ) -> M : ( N X. N ) --> ( Base ` R ) )
41 19 4 symgbasf1o 
 |-  ( q e. P -> q : N -1-1-onto-> N )
42 41 adantl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> q : N -1-1-onto-> N )
43 f1of 
 |-  ( q : N -1-1-onto-> N -> q : N --> N )
44 42 43 syl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> q : N --> N )
45 44 ffvelrnda 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) /\ y e. N ) -> ( q ` y ) e. N )
46 simpr 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) /\ y e. N ) -> y e. N )
47 40 45 46 fovrnd 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) /\ y e. N ) -> ( ( q ` y ) M y ) e. ( Base ` R ) )
48 47 ralrimiva 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> A. y e. N ( ( q ` y ) M y ) e. ( Base ` R ) )
49 32 34 35 48 gsummptcl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) e. ( Base ` R ) )
50 11 7 ringcl 
 |-  ( ( R e. Ring /\ ( ( Y o. S ) ` q ) e. ( Base ` R ) /\ ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) e. ( Base ` R ) ) -> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) e. ( Base ` R ) )
51 22 31 49 50 syl3anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ q e. P ) -> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) e. ( Base ` R ) )
52 51 ralrimiva 
 |-  ( ( R e. CRing /\ M e. B ) -> A. q e. P ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) e. ( Base ` R ) )
53 eqid 
 |-  ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) = ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) )
54 eqid 
 |-  ( invg ` ( SymGrp ` N ) ) = ( invg ` ( SymGrp ` N ) )
55 19 symggrp 
 |-  ( N e. Fin -> ( SymGrp ` N ) e. Grp )
56 18 55 syl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( SymGrp ` N ) e. Grp )
57 4 54 56 grpinvf1o 
 |-  ( ( R e. CRing /\ M e. B ) -> ( invg ` ( SymGrp ` N ) ) : P -1-1-onto-> P )
58 11 15 21 52 53 57 gsummptfif1o 
 |-  ( ( R e. CRing /\ M e. B ) -> ( R gsum ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) ) = ( R gsum ( ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) o. ( invg ` ( SymGrp ` N ) ) ) ) )
59 f1of 
 |-  ( ( invg ` ( SymGrp ` N ) ) : P -1-1-onto-> P -> ( invg ` ( SymGrp ` N ) ) : P --> P )
60 57 59 syl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( invg ` ( SymGrp ` N ) ) : P --> P )
61 60 ffvelrnda 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( ( invg ` ( SymGrp ` N ) ) ` p ) e. P )
62 60 feqmptd 
 |-  ( ( R e. CRing /\ M e. B ) -> ( invg ` ( SymGrp ` N ) ) = ( p e. P |-> ( ( invg ` ( SymGrp ` N ) ) ` p ) ) )
63 eqidd 
 |-  ( ( R e. CRing /\ M e. B ) -> ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) = ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) )
64 fveq2 
 |-  ( q = ( ( invg ` ( SymGrp ` N ) ) ` p ) -> ( ( Y o. S ) ` q ) = ( ( Y o. S ) ` ( ( invg ` ( SymGrp ` N ) ) ` p ) ) )
65 fveq1 
 |-  ( q = ( ( invg ` ( SymGrp ` N ) ) ` p ) -> ( q ` y ) = ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) )
66 65 oveq1d 
 |-  ( q = ( ( invg ` ( SymGrp ` N ) ) ` p ) -> ( ( q ` y ) M y ) = ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) )
67 66 mpteq2dv 
 |-  ( q = ( ( invg ` ( SymGrp ` N ) ) ` p ) -> ( y e. N |-> ( ( q ` y ) M y ) ) = ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) )
68 67 oveq2d 
 |-  ( q = ( ( invg ` ( SymGrp ` N ) ) ` p ) -> ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) = ( U gsum ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) ) )
69 64 68 oveq12d 
 |-  ( q = ( ( invg ` ( SymGrp ` N ) ) ` p ) -> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) = ( ( ( Y o. S ) ` ( ( invg ` ( SymGrp ` N ) ) ` p ) ) .x. ( U gsum ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) ) ) )
70 61 62 63 69 fmptco 
 |-  ( ( R e. CRing /\ M e. B ) -> ( ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) o. ( invg ` ( SymGrp ` N ) ) ) = ( p e. P |-> ( ( ( Y o. S ) ` ( ( invg ` ( SymGrp ` N ) ) ` p ) ) .x. ( U gsum ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) ) ) ) )
71 19 4 54 symginv 
 |-  ( p e. P -> ( ( invg ` ( SymGrp ` N ) ) ` p ) = `' p )
72 71 adantl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( ( invg ` ( SymGrp ` N ) ) ` p ) = `' p )
73 72 fveq2d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( ( Y o. S ) ` ( ( invg ` ( SymGrp ` N ) ) ` p ) ) = ( ( Y o. S ) ` `' p ) )
74 12 ad2antrr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> R e. Ring )
75 18 adantr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> N e. Fin )
76 simpr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> p e. P )
77 4 5 6 zrhpsgninv 
 |-  ( ( R e. Ring /\ N e. Fin /\ p e. P ) -> ( ( Y o. S ) ` `' p ) = ( ( Y o. S ) ` p ) )
78 74 75 76 77 syl3anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( ( Y o. S ) ` `' p ) = ( ( Y o. S ) ` p ) )
79 73 78 eqtrd 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( ( Y o. S ) ` ( ( invg ` ( SymGrp ` N ) ) ` p ) ) = ( ( Y o. S ) ` p ) )
80 eqid 
 |-  ( Base ` U ) = ( Base ` U )
81 33 ad2antrr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> U e. CMnd )
82 39 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ y e. N ) -> M : ( N X. N ) --> ( Base ` R ) )
83 71 ad2antlr 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ y e. N ) -> ( ( invg ` ( SymGrp ` N ) ) ` p ) = `' p )
84 83 fveq1d 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ y e. N ) -> ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) = ( `' p ` y ) )
85 19 4 symgbasf1o 
 |-  ( p e. P -> p : N -1-1-onto-> N )
86 85 adantl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> p : N -1-1-onto-> N )
87 f1ocnv 
 |-  ( p : N -1-1-onto-> N -> `' p : N -1-1-onto-> N )
88 f1of 
 |-  ( `' p : N -1-1-onto-> N -> `' p : N --> N )
89 86 87 88 3syl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> `' p : N --> N )
90 89 ffvelrnda 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ y e. N ) -> ( `' p ` y ) e. N )
91 84 90 eqeltrd 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ y e. N ) -> ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) e. N )
92 simpr 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ y e. N ) -> y e. N )
93 82 91 92 fovrnd 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ y e. N ) -> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) e. ( Base ` R ) )
94 93 32 eleqtrdi 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ y e. N ) -> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) e. ( Base ` U ) )
95 94 ralrimiva 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> A. y e. N ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) e. ( Base ` U ) )
96 eqid 
 |-  ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) = ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) )
97 80 81 75 95 96 86 gsummptfif1o 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( U gsum ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) ) = ( U gsum ( ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) o. p ) ) )
98 f1of 
 |-  ( p : N -1-1-onto-> N -> p : N --> N )
99 86 98 syl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> p : N --> N )
100 99 ffvelrnda 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ x e. N ) -> ( p ` x ) e. N )
101 99 feqmptd 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> p = ( x e. N |-> ( p ` x ) ) )
102 eqidd 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) = ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) )
103 fveq2 
 |-  ( y = ( p ` x ) -> ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) = ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` ( p ` x ) ) )
104 id 
 |-  ( y = ( p ` x ) -> y = ( p ` x ) )
105 103 104 oveq12d 
 |-  ( y = ( p ` x ) -> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) = ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` ( p ` x ) ) M ( p ` x ) ) )
106 100 101 102 105 fmptco 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) o. p ) = ( x e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` ( p ` x ) ) M ( p ` x ) ) ) )
107 71 ad2antlr 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ x e. N ) -> ( ( invg ` ( SymGrp ` N ) ) ` p ) = `' p )
108 107 fveq1d 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ x e. N ) -> ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` ( p ` x ) ) = ( `' p ` ( p ` x ) ) )
109 f1ocnvfv1 
 |-  ( ( p : N -1-1-onto-> N /\ x e. N ) -> ( `' p ` ( p ` x ) ) = x )
110 86 109 sylan 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ x e. N ) -> ( `' p ` ( p ` x ) ) = x )
111 108 110 eqtrd 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ x e. N ) -> ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` ( p ` x ) ) = x )
112 111 oveq1d 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) /\ x e. N ) -> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` ( p ` x ) ) M ( p ` x ) ) = ( x M ( p ` x ) ) )
113 112 mpteq2dva 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( x e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` ( p ` x ) ) M ( p ` x ) ) ) = ( x e. N |-> ( x M ( p ` x ) ) ) )
114 106 113 eqtrd 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) o. p ) = ( x e. N |-> ( x M ( p ` x ) ) ) )
115 114 oveq2d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( U gsum ( ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) o. p ) ) = ( U gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) )
116 97 115 eqtrd 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( U gsum ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) ) = ( U gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) )
117 79 116 oveq12d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ p e. P ) -> ( ( ( Y o. S ) ` ( ( invg ` ( SymGrp ` N ) ) ` p ) ) .x. ( U gsum ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) ) ) = ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) )
118 117 mpteq2dva 
 |-  ( ( R e. CRing /\ M e. B ) -> ( p e. P |-> ( ( ( Y o. S ) ` ( ( invg ` ( SymGrp ` N ) ) ` p ) ) .x. ( U gsum ( y e. N |-> ( ( ( ( invg ` ( SymGrp ` N ) ) ` p ) ` y ) M y ) ) ) ) ) = ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) ) )
119 70 118 eqtrd 
 |-  ( ( R e. CRing /\ M e. B ) -> ( ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) o. ( invg ` ( SymGrp ` N ) ) ) = ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) ) )
120 119 oveq2d 
 |-  ( ( R e. CRing /\ M e. B ) -> ( R gsum ( ( q e. P |-> ( ( ( Y o. S ) ` q ) .x. ( U gsum ( y e. N |-> ( ( q ` y ) M y ) ) ) ) ) o. ( invg ` ( SymGrp ` N ) ) ) ) = ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) ) ) )
121 10 58 120 3eqtrd 
 |-  ( ( R e. CRing /\ M e. B ) -> ( D ` M ) = ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) ) ) )