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