Metamath Proof Explorer

Theorem mdetpmtr1

Description: The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypotheses mdetpmtr.a 
|- A = ( N Mat R )
mdetpmtr.b 
|- B = ( Base ` A )
mdetpmtr.d 
|- D = ( N maDet R )
mdetpmtr.g 
|- G = ( Base ` ( SymGrp ` N ) )
mdetpmtr.s 
|- S = ( pmSgn ` N )
mdetpmtr.z 
|- Z = ( ZRHom ` R )
mdetpmtr.t 
|- .x. = ( .r ` R )
mdetpmtr1.e 
|- E = ( i e. N , j e. N |-> ( ( P ` i ) M j ) )
Assertion mdetpmtr1 
|- ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` E ) ) )

Proof

Step Hyp Ref Expression
1 mdetpmtr.a 
 |-  A = ( N Mat R )
2 mdetpmtr.b 
 |-  B = ( Base ` A )
3 mdetpmtr.d 
 |-  D = ( N maDet R )
4 mdetpmtr.g 
 |-  G = ( Base ` ( SymGrp ` N ) )
5 mdetpmtr.s 
 |-  S = ( pmSgn ` N )
6 mdetpmtr.z 
 |-  Z = ( ZRHom ` R )
7 mdetpmtr.t 
 |-  .x. = ( .r ` R )
8 mdetpmtr1.e 
 |-  E = ( i e. N , j e. N |-> ( ( P ` i ) M j ) )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
11 crngring 
 |-  ( R e. CRing -> R e. Ring )
12 11 ad2antrr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> R e. Ring )
13 4 fvexi 
 |-  G e. _V
14 13 a1i 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> G e. _V )
15 simplr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> N e. Fin )
16 5 4 psgndmfi 
 |-  ( N e. Fin -> S Fn G )
17 fnfun 
 |-  ( S Fn G -> Fun S )
18 15 16 17 3syl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> Fun S )
19 simprr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> P e. G )
20 fndm 
 |-  ( S Fn G -> dom S = G )
21 15 16 20 3syl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> dom S = G )
22 19 21 eleqtrrd 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> P e. dom S )
23 fvco 
 |-  ( ( Fun S /\ P e. dom S ) -> ( ( Z o. S ) ` P ) = ( Z ` ( S ` P ) ) )
24 18 22 23 syl2anc 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( ( Z o. S ) ` P ) = ( Z ` ( S ` P ) ) )
25 4 5 6 zrhpsgnelbas 
 |-  ( ( R e. Ring /\ N e. Fin /\ P e. G ) -> ( Z ` ( S ` P ) ) e. ( Base ` R ) )
26 12 15 19 25 syl3anc 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( Z ` ( S ` P ) ) e. ( Base ` R ) )
27 24 26 eqeltrd 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( ( Z o. S ) ` P ) e. ( Base ` R ) )
28 12 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> R e. Ring )
29 4 5 cofipsgn 
 |-  ( ( N e. Fin /\ p e. G ) -> ( ( Z o. S ) ` p ) = ( Z ` ( S ` p ) ) )
30 15 29 sylan 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( Z o. S ) ` p ) = ( Z ` ( S ` p ) ) )
31 simpllr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> N e. Fin )
32 simpr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> p e. G )
33 4 5 6 zrhpsgnelbas 
 |-  ( ( R e. Ring /\ N e. Fin /\ p e. G ) -> ( Z ` ( S ` p ) ) e. ( Base ` R ) )
34 28 31 32 33 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( Z ` ( S ` p ) ) e. ( Base ` R ) )
35 30 34 eqeltrd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( Z o. S ) ` p ) e. ( Base ` R ) )
36 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
37 36 9 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
38 36 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
39 38 ad3antrrr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( mulGrp ` R ) e. CMnd )
40 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
41 40 4 symgfv 
 |-  ( ( p e. G /\ x e. N ) -> ( p ` x ) e. N )
42 41 adantll 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) -> ( p ` x ) e. N )
43 simpr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) -> x e. N )
44 simpll 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> R e. CRing )
45 simp1rr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> P e. G )
46 simp2 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> i e. N )
47 40 4 symgfv 
 |-  ( ( P e. G /\ i e. N ) -> ( P ` i ) e. N )
48 45 46 47 syl2anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> ( P ` i ) e. N )
49 simp3 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> j e. N )
50 simp1rl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> M e. B )
51 1 9 2 48 49 50 matecld 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> ( ( P ` i ) M j ) e. ( Base ` R ) )
52 1 9 2 15 44 51 matbas2d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( i e. N , j e. N |-> ( ( P ` i ) M j ) ) e. B )
53 8 52 eqeltrid 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> E e. B )
54 53 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) -> E e. B )
55 1 9 2 42 43 54 matecld 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) -> ( ( p ` x ) E x ) e. ( Base ` R ) )
56 55 ralrimiva 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> A. x e. N ( ( p ` x ) E x ) e. ( Base ` R ) )
57 37 39 31 56 gsummptcl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) e. ( Base ` R ) )
58 9 7 ringcl 
 |-  ( ( R e. Ring /\ ( ( Z o. S ) ` p ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) e. ( Base ` R ) ) -> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) e. ( Base ` R ) )
59 28 35 57 58 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) e. ( Base ` R ) )
60 eqid 
 |-  ( p e. G |-> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) = ( p e. G |-> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) )
61 40 4 symgbasfi 
 |-  ( N e. Fin -> G e. Fin )
62 15 61 syl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> G e. Fin )
63 ovexd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) e. _V )
64 fvexd 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( 0g ` R ) e. _V )
65 60 62 63 64 fsuppmptdm 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( p e. G |-> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) finSupp ( 0g ` R ) )
66 9 10 7 12 14 27 59 65 gsummulc2 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) ) ) = ( ( ( Z o. S ) ` P ) .x. ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) ) ) )
67 nfcv 
 |-  F/_ q ( ( ( Z o. S ) ` ( P o. p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) )
68 fveq2 
 |-  ( q = ( P o. p ) -> ( ( Z o. S ) ` q ) = ( ( Z o. S ) ` ( P o. p ) ) )
69 fveq1 
 |-  ( q = ( P o. p ) -> ( q ` x ) = ( ( P o. p ) ` x ) )
70 69 oveq1d 
 |-  ( q = ( P o. p ) -> ( ( q ` x ) M x ) = ( ( ( P o. p ) ` x ) M x ) )
71 70 mpteq2dv 
 |-  ( q = ( P o. p ) -> ( x e. N |-> ( ( q ` x ) M x ) ) = ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) )
72 71 oveq2d 
 |-  ( q = ( P o. p ) -> ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) = ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) )
73 68 72 oveq12d 
 |-  ( q = ( P o. p ) -> ( ( ( Z o. S ) ` q ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) ) = ( ( ( Z o. S ) ` ( P o. p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) ) )
74 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
75 12 74 syl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> R e. CMnd )
76 ssidd 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( Base ` R ) C_ ( Base ` R ) )
77 12 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> R e. Ring )
78 4 5 cofipsgn 
 |-  ( ( N e. Fin /\ q e. G ) -> ( ( Z o. S ) ` q ) = ( Z ` ( S ` q ) ) )
79 15 78 sylan 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> ( ( Z o. S ) ` q ) = ( Z ` ( S ` q ) ) )
80 simpllr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> N e. Fin )
81 simpr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> q e. G )
82 4 5 6 zrhpsgnelbas 
 |-  ( ( R e. Ring /\ N e. Fin /\ q e. G ) -> ( Z ` ( S ` q ) ) e. ( Base ` R ) )
83 77 80 81 82 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> ( Z ` ( S ` q ) ) e. ( Base ` R ) )
84 79 83 eqeltrd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> ( ( Z o. S ) ` q ) e. ( Base ` R ) )
85 38 ad3antrrr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> ( mulGrp ` R ) e. CMnd )
86 40 4 symgfv 
 |-  ( ( q e. G /\ x e. N ) -> ( q ` x ) e. N )
87 86 adantll 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) /\ x e. N ) -> ( q ` x ) e. N )
88 simpr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) /\ x e. N ) -> x e. N )
89 simprl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> M e. B )
90 89 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) /\ x e. N ) -> M e. B )
91 1 9 2 87 88 90 matecld 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) /\ x e. N ) -> ( ( q ` x ) M x ) e. ( Base ` R ) )
92 91 ralrimiva 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> A. x e. N ( ( q ` x ) M x ) e. ( Base ` R ) )
93 37 85 80 92 gsummptcl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) e. ( Base ` R ) )
94 9 7 ringcl 
 |-  ( ( R e. Ring /\ ( ( Z o. S ) ` q ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) e. ( Base ` R ) ) -> ( ( ( Z o. S ) ` q ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) ) e. ( Base ` R ) )
95 77 84 93 94 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> ( ( ( Z o. S ) ` q ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) ) e. ( Base ` R ) )
96 eqid 
 |-  ( +g ` ( SymGrp ` N ) ) = ( +g ` ( SymGrp ` N ) )
97 40 4 96 symgov 
 |-  ( ( P e. G /\ p e. G ) -> ( P ( +g ` ( SymGrp ` N ) ) p ) = ( P o. p ) )
98 40 4 96 symgcl 
 |-  ( ( P e. G /\ p e. G ) -> ( P ( +g ` ( SymGrp ` N ) ) p ) e. G )
99 97 98 eqeltrrd 
 |-  ( ( P e. G /\ p e. G ) -> ( P o. p ) e. G )
100 19 99 sylan 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( P o. p ) e. G )
101 19 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> P e. G )
102 4 symgfcoeu 
 |-  ( ( N e. Fin /\ P e. G /\ q e. G ) -> E! p e. G q = ( P o. p ) )
103 80 101 81 102 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ q e. G ) -> E! p e. G q = ( P o. p ) )
104 67 9 10 73 75 62 76 95 100 103 gsummptf1o 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( R gsum ( q e. G |-> ( ( ( Z o. S ) ` q ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) ) ) ) = ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` ( P o. p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) ) ) ) )
105 3 1 2 4 6 5 7 36 mdetleib 
 |-  ( M e. B -> ( D ` M ) = ( R gsum ( q e. G |-> ( ( ( Z o. S ) ` q ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) ) ) ) )
106 105 ad2antrl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( R gsum ( q e. G |-> ( ( ( Z o. S ) ` q ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( q ` x ) M x ) ) ) ) ) ) )
107 27 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( Z o. S ) ` P ) e. ( Base ` R ) )
108 9 7 ringass 
 |-  ( ( R e. Ring /\ ( ( ( Z o. S ) ` P ) e. ( Base ` R ) /\ ( ( Z o. S ) ` p ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) e. ( Base ` R ) ) ) -> ( ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) = ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) )
109 28 107 35 57 108 syl13anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) = ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) )
110 24 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( Z o. S ) ` P ) = ( Z ` ( S ` P ) ) )
111 110 30 oveq12d 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` p ) ) = ( ( Z ` ( S ` P ) ) .x. ( Z ` ( S ` p ) ) ) )
112 4 5 cofipsgn 
 |-  ( ( N e. Fin /\ ( P o. p ) e. G ) -> ( ( Z o. S ) ` ( P o. p ) ) = ( Z ` ( S ` ( P o. p ) ) ) )
113 31 100 112 syl2anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( Z o. S ) ` ( P o. p ) ) = ( Z ` ( S ` ( P o. p ) ) ) )
114 19 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> P e. G )
115 40 5 4 psgnco 
 |-  ( ( N e. Fin /\ P e. G /\ p e. G ) -> ( S ` ( P o. p ) ) = ( ( S ` P ) x. ( S ` p ) ) )
116 31 114 32 115 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( S ` ( P o. p ) ) = ( ( S ` P ) x. ( S ` p ) ) )
117 116 fveq2d 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( Z ` ( S ` ( P o. p ) ) ) = ( Z ` ( ( S ` P ) x. ( S ` p ) ) ) )
118 6 zrhrhm 
 |-  ( R e. Ring -> Z e. ( ZZring RingHom R ) )
119 12 118 syl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> Z e. ( ZZring RingHom R ) )
120 119 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> Z e. ( ZZring RingHom R ) )
121 1z 
 |-  1 e. ZZ
122 neg1z 
 |-  -u 1 e. ZZ
123 prssi 
 |-  ( ( 1 e. ZZ /\ -u 1 e. ZZ ) -> { 1 , -u 1 } C_ ZZ )
124 121 122 123 mp2an 
 |-  { 1 , -u 1 } C_ ZZ
125 4 5 psgnran 
 |-  ( ( N e. Fin /\ P e. G ) -> ( S ` P ) e. { 1 , -u 1 } )
126 31 114 125 syl2anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( S ` P ) e. { 1 , -u 1 } )
127 124 126 sselid 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( S ` P ) e. ZZ )
128 4 5 psgnran 
 |-  ( ( N e. Fin /\ p e. G ) -> ( S ` p ) e. { 1 , -u 1 } )
129 15 128 sylan 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( S ` p ) e. { 1 , -u 1 } )
130 124 129 sselid 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( S ` p ) e. ZZ )
131 zringbas 
 |-  ZZ = ( Base ` ZZring )
132 zringmulr 
 |-  x. = ( .r ` ZZring )
133 131 132 7 rhmmul 
 |-  ( ( Z e. ( ZZring RingHom R ) /\ ( S ` P ) e. ZZ /\ ( S ` p ) e. ZZ ) -> ( Z ` ( ( S ` P ) x. ( S ` p ) ) ) = ( ( Z ` ( S ` P ) ) .x. ( Z ` ( S ` p ) ) ) )
134 120 127 130 133 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( Z ` ( ( S ` P ) x. ( S ` p ) ) ) = ( ( Z ` ( S ` P ) ) .x. ( Z ` ( S ` p ) ) ) )
135 113 117 134 3eqtrrd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( Z ` ( S ` P ) ) .x. ( Z ` ( S ` p ) ) ) = ( ( Z o. S ) ` ( P o. p ) ) )
136 111 135 eqtrd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` p ) ) = ( ( Z o. S ) ` ( P o. p ) ) )
137 8 a1i 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) -> E = ( i e. N , j e. N |-> ( ( P ` i ) M j ) ) )
138 simprl 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> i = ( p ` x ) )
139 138 fveq2d 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> ( P ` i ) = ( P ` ( p ` x ) ) )
140 simpllr 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> p e. G )
141 40 4 symgbasf 
 |-  ( p e. G -> p : N --> N )
142 ffun 
 |-  ( p : N --> N -> Fun p )
143 140 141 142 3syl 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> Fun p )
144 simplr 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> x e. N )
145 fdm 
 |-  ( p : N --> N -> dom p = N )
146 140 141 145 3syl 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> dom p = N )
147 144 146 eleqtrrd 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> x e. dom p )
148 fvco 
 |-  ( ( Fun p /\ x e. dom p ) -> ( ( P o. p ) ` x ) = ( P ` ( p ` x ) ) )
149 143 147 148 syl2anc 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> ( ( P o. p ) ` x ) = ( P ` ( p ` x ) ) )
150 139 149 eqtr4d 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> ( P ` i ) = ( ( P o. p ) ` x ) )
151 simprr 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> j = x )
152 150 151 oveq12d 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) /\ ( i = ( p ` x ) /\ j = x ) ) -> ( ( P ` i ) M j ) = ( ( ( P o. p ) ` x ) M x ) )
153 ovexd 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) -> ( ( ( P o. p ) ` x ) M x ) e. _V )
154 137 152 42 43 153 ovmpod 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) /\ x e. N ) -> ( ( p ` x ) E x ) = ( ( ( P o. p ) ` x ) M x ) )
155 154 mpteq2dva 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( x e. N |-> ( ( p ` x ) E x ) ) = ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) )
156 155 oveq2d 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) = ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) )
157 136 156 oveq12d 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) = ( ( ( Z o. S ) ` ( P o. p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) ) )
158 109 157 eqtr3d 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ p e. G ) -> ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) = ( ( ( Z o. S ) ` ( P o. p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) ) )
159 158 mpteq2dva 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( p e. G |-> ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) ) = ( p e. G |-> ( ( ( Z o. S ) ` ( P o. p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) ) ) )
160 159 oveq2d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) ) ) = ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` ( P o. p ) ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( ( P o. p ) ` x ) M x ) ) ) ) ) ) )
161 104 106 160 3eqtr4d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) ) ) )
162 3 1 2 4 6 5 7 36 mdetleib 
 |-  ( E e. B -> ( D ` E ) = ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) ) )
163 53 162 syl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` E ) = ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) ) )
164 163 oveq2d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( ( ( Z o. S ) ` P ) .x. ( D ` E ) ) = ( ( ( Z o. S ) ` P ) .x. ( R gsum ( p e. G |-> ( ( ( Z o. S ) ` p ) .x. ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) E x ) ) ) ) ) ) ) )
165 66 161 164 3eqtr4d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` E ) ) )