MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetrsca Structured version   Unicode version

Theorem mdetrsca 19624
Description: The determinant function is homogeneous for each row: The matrices X and Z are identical except for the I's row, and the I's row of the matrix X is the componentwise product of the I's row of the matrix Z and the scalar Y. In this case the determinant of X is the determinant of Z multiplied by Y. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
Hypotheses
Ref Expression
mdetrsca.d  |-  D  =  ( N maDet  R )
mdetrsca.a  |-  A  =  ( N Mat  R )
mdetrsca.b  |-  B  =  ( Base `  A
)
mdetrsca.k  |-  K  =  ( Base `  R
)
mdetrsca.t  |-  .x.  =  ( .r `  R )
mdetrsca.r  |-  ( ph  ->  R  e.  CRing )
mdetrsca.x  |-  ( ph  ->  X  e.  B )
mdetrsca.y  |-  ( ph  ->  Y  e.  K )
mdetrsca.z  |-  ( ph  ->  Z  e.  B )
mdetrsca.i  |-  ( ph  ->  I  e.  N )
mdetrsca.eq  |-  ( ph  ->  ( X  |`  ( { I }  X.  N ) )  =  ( ( ( { I }  X.  N
)  X.  { Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) )
mdetrsca.ne  |-  ( ph  ->  ( X  |`  (
( N  \  {
I } )  X.  N ) )  =  ( Z  |`  (
( N  \  {
I } )  X.  N ) ) )
Assertion
Ref Expression
mdetrsca  |-  ( ph  ->  ( D `  X
)  =  ( Y 
.x.  ( D `  Z ) ) )

Proof of Theorem mdetrsca
Dummy variables  p  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetrsca.eq . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  |`  ( { I }  X.  N ) )  =  ( ( ( { I }  X.  N
)  X.  { Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) )
21oveqd 6321 . . . . . . . . . . . . 13  |-  ( ph  ->  ( I ( X  |`  ( { I }  X.  N ) ) ( p `  I ) )  =  ( I ( ( ( { I }  X.  N
)  X.  { Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) ( p `  I
) ) )
32adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( I ( X  |`  ( {
I }  X.  N
) ) ( p `
 I ) )  =  ( I ( ( ( { I }  X.  N )  X. 
{ Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) ( p `  I ) ) )
4 mdetrsca.i . . . . . . . . . . . . . . 15  |-  ( ph  ->  I  e.  N )
54adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  I  e.  N
)
6 snidg 4024 . . . . . . . . . . . . . 14  |-  ( I  e.  N  ->  I  e.  { I } )
75, 6syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  I  e.  {
I } )
8 eqid 2423 . . . . . . . . . . . . . . . . 17  |-  ( SymGrp `  N )  =  (
SymGrp `  N )
9 eqid 2423 . . . . . . . . . . . . . . . . 17  |-  ( Base `  ( SymGrp `  N )
)  =  ( Base `  ( SymGrp `  N )
)
108, 9symgbasf1o 17021 . . . . . . . . . . . . . . . 16  |-  ( p  e.  ( Base `  ( SymGrp `
 N ) )  ->  p : N -1-1-onto-> N
)
1110adantl 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  p : N -1-1-onto-> N
)
12 f1of 5830 . . . . . . . . . . . . . . 15  |-  ( p : N -1-1-onto-> N  ->  p : N
--> N )
1311, 12syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  p : N --> N )
1413, 5ffvelrnd 6037 . . . . . . . . . . . . 13  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( p `  I )  e.  N
)
15 ovres 6449 . . . . . . . . . . . . 13  |-  ( ( I  e.  { I }  /\  ( p `  I )  e.  N
)  ->  ( I
( X  |`  ( { I }  X.  N ) ) ( p `  I ) )  =  ( I X ( p `  I ) ) )
167, 14, 15syl2anc 666 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( I ( X  |`  ( {
I }  X.  N
) ) ( p `
 I ) )  =  ( I X ( p `  I
) ) )
17 opelxpi 4884 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  { I }  /\  ( p `  I )  e.  N
)  ->  <. I ,  ( p `  I
) >.  e.  ( { I }  X.  N
) )
187, 14, 17syl2anc 666 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  <. I ,  ( p `  I )
>.  e.  ( { I }  X.  N ) )
19 snfi 7659 . . . . . . . . . . . . . . . 16  |-  { I }  e.  Fin
20 mdetrsca.x . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  e.  B )
21 mdetrsca.a . . . . . . . . . . . . . . . . . . . 20  |-  A  =  ( N Mat  R )
22 mdetrsca.b . . . . . . . . . . . . . . . . . . . 20  |-  B  =  ( Base `  A
)
2321, 22matrcl 19433 . . . . . . . . . . . . . . . . . . 19  |-  ( X  e.  B  ->  ( N  e.  Fin  /\  R  e.  _V ) )
2420, 23syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( N  e.  Fin  /\  R  e.  _V )
)
2524simpld 461 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  Fin )
2625adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  N  e.  Fin )
27 xpfi 7850 . . . . . . . . . . . . . . . 16  |-  ( ( { I }  e.  Fin  /\  N  e.  Fin )  ->  ( { I }  X.  N )  e. 
Fin )
2819, 26, 27sylancr 668 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( { I }  X.  N )  e. 
Fin )
29 mdetrsca.y . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Y  e.  K )
3029adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  Y  e.  K
)
31 mdetrsca.z . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Z  e.  B )
32 mdetrsca.k . . . . . . . . . . . . . . . . . . . 20  |-  K  =  ( Base `  R
)
3321, 32, 22matbas2i 19443 . . . . . . . . . . . . . . . . . . 19  |-  ( Z  e.  B  ->  Z  e.  ( K  ^m  ( N  X.  N ) ) )
34 elmapi 7503 . . . . . . . . . . . . . . . . . . 19  |-  ( Z  e.  ( K  ^m  ( N  X.  N
) )  ->  Z : ( N  X.  N ) --> K )
3531, 33, 343syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Z : ( N  X.  N ) --> K )
3635adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  Z : ( N  X.  N ) --> K )
37 ffn 5745 . . . . . . . . . . . . . . . . 17  |-  ( Z : ( N  X.  N ) --> K  ->  Z  Fn  ( N  X.  N ) )
3836, 37syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  Z  Fn  ( N  X.  N ) )
395snssd 4144 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  { I }  C_  N )
40 xpss1 4961 . . . . . . . . . . . . . . . . 17  |-  ( { I }  C_  N  ->  ( { I }  X.  N )  C_  ( N  X.  N ) )
4139, 40syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( { I }  X.  N )  C_  ( N  X.  N
) )
42 fnssres 5706 . . . . . . . . . . . . . . . 16  |-  ( ( Z  Fn  ( N  X.  N )  /\  ( { I }  X.  N )  C_  ( N  X.  N ) )  ->  ( Z  |`  ( { I }  X.  N ) )  Fn  ( { I }  X.  N ) )
4338, 41, 42syl2anc 666 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( Z  |`  ( { I }  X.  N ) )  Fn  ( { I }  X.  N ) )
44 eqidd 2424 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  <. I ,  ( p `  I
) >.  e.  ( { I }  X.  N
) )  ->  (
( Z  |`  ( { I }  X.  N ) ) `  <. I ,  ( p `
 I ) >.
)  =  ( ( Z  |`  ( {
I }  X.  N
) ) `  <. I ,  ( p `  I ) >. )
)
4528, 30, 43, 44ofc1 6567 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  <. I ,  ( p `  I
) >.  e.  ( { I }  X.  N
) )  ->  (
( ( ( { I }  X.  N
)  X.  { Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) `
 <. I ,  ( p `  I )
>. )  =  ( Y  .x.  ( ( Z  |`  ( { I }  X.  N ) ) `  <. I ,  ( p `
 I ) >.
) ) )
4618, 45mpdan 673 . . . . . . . . . . . . 13  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( { I }  X.  N )  X.  { Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) `
 <. I ,  ( p `  I )
>. )  =  ( Y  .x.  ( ( Z  |`  ( { I }  X.  N ) ) `  <. I ,  ( p `
 I ) >.
) ) )
47 df-ov 6307 . . . . . . . . . . . . 13  |-  ( I ( ( ( { I }  X.  N
)  X.  { Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) ( p `  I
) )  =  ( ( ( ( { I }  X.  N
)  X.  { Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) `
 <. I ,  ( p `  I )
>. )
48 df-ov 6307 . . . . . . . . . . . . . 14  |-  ( I ( Z  |`  ( { I }  X.  N ) ) ( p `  I ) )  =  ( ( Z  |`  ( {
I }  X.  N
) ) `  <. I ,  ( p `  I ) >. )
4948oveq2i 6315 . . . . . . . . . . . . 13  |-  ( Y 
.x.  ( I ( Z  |`  ( {
I }  X.  N
) ) ( p `
 I ) ) )  =  ( Y 
.x.  ( ( Z  |`  ( { I }  X.  N ) ) `  <. I ,  ( p `
 I ) >.
) )
5046, 47, 493eqtr4g 2489 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( I ( ( ( { I }  X.  N )  X. 
{ Y } )  oF  .x.  ( Z  |`  ( { I }  X.  N ) ) ) ( p `  I ) )  =  ( Y  .x.  (
I ( Z  |`  ( { I }  X.  N ) ) ( p `  I ) ) ) )
513, 16, 503eqtr3d 2472 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( I X ( p `  I
) )  =  ( Y  .x.  ( I ( Z  |`  ( { I }  X.  N ) ) ( p `  I ) ) ) )
52 ovres 6449 . . . . . . . . . . . . 13  |-  ( ( I  e.  { I }  /\  ( p `  I )  e.  N
)  ->  ( I
( Z  |`  ( { I }  X.  N ) ) ( p `  I ) )  =  ( I Z ( p `  I ) ) )
537, 14, 52syl2anc 666 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( I ( Z  |`  ( {
I }  X.  N
) ) ( p `
 I ) )  =  ( I Z ( p `  I
) ) )
5453oveq2d 6320 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( Y  .x.  ( I ( Z  |`  ( { I }  X.  N ) ) ( p `  I ) ) )  =  ( Y  .x.  ( I Z ( p `  I ) ) ) )
5551, 54eqtrd 2464 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( I X ( p `  I
) )  =  ( Y  .x.  ( I Z ( p `  I ) ) ) )
5655oveq1d 6319 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( I X ( p `  I ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) )  =  ( ( Y  .x.  ( I Z ( p `  I ) ) ) 
.x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r Z ( p `  r ) ) ) ) ) )
57 mdetrsca.r . . . . . . . . . . . 12  |-  ( ph  ->  R  e.  CRing )
58 crngring 17788 . . . . . . . . . . . 12  |-  ( R  e.  CRing  ->  R  e.  Ring )
5957, 58syl 17 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  Ring )
6059adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  R  e.  Ring )
6136, 5, 14fovrnd 6454 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( I Z ( p `  I
) )  e.  K
)
62 eqid 2423 . . . . . . . . . . . 12  |-  (mulGrp `  R )  =  (mulGrp `  R )
6362, 32mgpbas 17726 . . . . . . . . . . 11  |-  K  =  ( Base `  (mulGrp `  R ) )
6462crngmgp 17785 . . . . . . . . . . . . 13  |-  ( R  e.  CRing  ->  (mulGrp `  R
)  e. CMnd )
6557, 64syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  (mulGrp `  R )  e. CMnd )
6665adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  (mulGrp `  R )  e. CMnd )
67 difssd 3595 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( N  \  { I } ) 
C_  N )
68 ssfi 7800 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  ( N  \  { I } )  C_  N
)  ->  ( N  \  { I } )  e.  Fin )
6926, 67, 68syl2anc 666 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( N  \  { I } )  e.  Fin )
70 eldifi 3589 . . . . . . . . . . . . 13  |-  ( r  e.  ( N  \  { I } )  ->  r  e.  N
)
7135ad2antrr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  N )  ->  Z : ( N  X.  N ) --> K )
72 simpr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  N )  ->  r  e.  N )
7313ffvelrnda 6036 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  N )  ->  (
p `  r )  e.  N )
7471, 72, 73fovrnd 6454 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  N )  ->  (
r Z ( p `
 r ) )  e.  K )
7570, 74sylan2 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  ( N  \  {
I } ) )  ->  ( r Z ( p `  r
) )  e.  K
)
7675ralrimiva 2840 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  A. r  e.  ( N  \  { I } ) ( r Z ( p `  r ) )  e.  K )
7763, 66, 69, 76gsummptcl 17596 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r Z ( p `  r ) ) ) )  e.  K )
78 mdetrsca.t . . . . . . . . . . 11  |-  .x.  =  ( .r `  R )
7932, 78ringass 17794 . . . . . . . . . 10  |-  ( ( R  e.  Ring  /\  ( Y  e.  K  /\  ( I Z ( p `  I ) )  e.  K  /\  ( (mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) )  e.  K ) )  ->  ( ( Y 
.x.  ( I Z ( p `  I
) ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) )  =  ( Y 
.x.  ( ( I Z ( p `  I ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) ) ) )
8060, 30, 61, 77, 79syl13anc 1267 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( Y 
.x.  ( I Z ( p `  I
) ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) )  =  ( Y 
.x.  ( ( I Z ( p `  I ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) ) ) )
8156, 80eqtrd 2464 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( I X ( p `  I ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) )  =  ( Y 
.x.  ( ( I Z ( p `  I ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) ) ) )
8262, 78mgpplusg 17724 . . . . . . . . . 10  |-  .x.  =  ( +g  `  (mulGrp `  R ) )
8321, 32, 22matbas2i 19443 . . . . . . . . . . . . 13  |-  ( X  e.  B  ->  X  e.  ( K  ^m  ( N  X.  N ) ) )
84 elmapi 7503 . . . . . . . . . . . . 13  |-  ( X  e.  ( K  ^m  ( N  X.  N
) )  ->  X : ( N  X.  N ) --> K )
8520, 83, 843syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  X : ( N  X.  N ) --> K )
8685ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  N )  ->  X : ( N  X.  N ) --> K )
8786, 72, 73fovrnd 6454 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  N )  ->  (
r X ( p `
 r ) )  e.  K )
88 disjdif 3869 . . . . . . . . . . 11  |-  ( { I }  i^i  ( N  \  { I }
) )  =  (/)
8988a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( { I }  i^i  ( N  \  { I } ) )  =  (/) )
90 undif 3878 . . . . . . . . . . . 12  |-  ( { I }  C_  N  <->  ( { I }  u.  ( N  \  { I } ) )  =  N )
9139, 90sylib 200 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( { I }  u.  ( N  \  { I } ) )  =  N )
9291eqcomd 2431 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  N  =  ( { I }  u.  ( N  \  { I } ) ) )
9363, 82, 66, 26, 87, 89, 92gsummptfidmsplit 17560 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `  r ) ) ) )  =  ( ( (mulGrp `  R )  gsumg  ( r  e.  {
I }  |->  ( r X ( p `  r ) ) ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r X ( p `  r ) ) ) ) ) )
94 cmnmnd 17442 . . . . . . . . . . . 12  |-  ( (mulGrp `  R )  e. CMnd  ->  (mulGrp `  R )  e.  Mnd )
9566, 94syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  (mulGrp `  R )  e.  Mnd )
9685adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  X : ( N  X.  N ) --> K )
9796, 5, 14fovrnd 6454 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( I X ( p `  I
) )  e.  K
)
98 id 23 . . . . . . . . . . . . 13  |-  ( r  =  I  ->  r  =  I )
99 fveq2 5880 . . . . . . . . . . . . 13  |-  ( r  =  I  ->  (
p `  r )  =  ( p `  I ) )
10098, 99oveq12d 6322 . . . . . . . . . . . 12  |-  ( r  =  I  ->  (
r X ( p `
 r ) )  =  ( I X ( p `  I
) ) )
10163, 100gsumsn 17584 . . . . . . . . . . 11  |-  ( ( (mulGrp `  R )  e.  Mnd  /\  I  e.  N  /\  ( I X ( p `  I ) )  e.  K )  ->  (
(mulGrp `  R )  gsumg  ( r  e.  { I }  |->  ( r X ( p `  r
) ) ) )  =  ( I X ( p `  I
) ) )
10295, 5, 97, 101syl3anc 1265 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  {
I }  |->  ( r X ( p `  r ) ) ) )  =  ( I X ( p `  I ) ) )
103 mdetrsca.ne . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  |`  (
( N  \  {
I } )  X.  N ) )  =  ( Z  |`  (
( N  \  {
I } )  X.  N ) ) )
104103oveqd 6321 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( r ( X  |`  ( ( N  \  { I } )  X.  N ) ) ( p `  r
) )  =  ( r ( Z  |`  ( ( N  \  { I } )  X.  N ) ) ( p `  r
) ) )
105104ad2antrr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  ( N  \  {
I } ) )  ->  ( r ( X  |`  ( ( N  \  { I }
)  X.  N ) ) ( p `  r ) )  =  ( r ( Z  |`  ( ( N  \  { I } )  X.  N ) ) ( p `  r
) ) )
106 simpr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  ( N  \  {
I } ) )  ->  r  e.  ( N  \  { I } ) )
10770, 73sylan2 477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  ( N  \  {
I } ) )  ->  ( p `  r )  e.  N
)
108 ovres 6449 . . . . . . . . . . . . . 14  |-  ( ( r  e.  ( N 
\  { I }
)  /\  ( p `  r )  e.  N
)  ->  ( r
( X  |`  (
( N  \  {
I } )  X.  N ) ) ( p `  r ) )  =  ( r X ( p `  r ) ) )
109106, 107, 108syl2anc 666 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  ( N  \  {
I } ) )  ->  ( r ( X  |`  ( ( N  \  { I }
)  X.  N ) ) ( p `  r ) )  =  ( r X ( p `  r ) ) )
110 ovres 6449 . . . . . . . . . . . . . 14  |-  ( ( r  e.  ( N 
\  { I }
)  /\  ( p `  r )  e.  N
)  ->  ( r
( Z  |`  (
( N  \  {
I } )  X.  N ) ) ( p `  r ) )  =  ( r Z ( p `  r ) ) )
111106, 107, 110syl2anc 666 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  ( N  \  {
I } ) )  ->  ( r ( Z  |`  ( ( N  \  { I }
)  X.  N ) ) ( p `  r ) )  =  ( r Z ( p `  r ) ) )
112105, 109, 1113eqtr3d 2472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  r  e.  ( N  \  {
I } ) )  ->  ( r X ( p `  r
) )  =  ( r Z ( p `
 r ) ) )
113112mpteq2dva 4509 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( r  e.  ( N  \  {
I } )  |->  ( r X ( p `
 r ) ) )  =  ( r  e.  ( N  \  { I } ) 
|->  ( r Z ( p `  r ) ) ) )
114113oveq2d 6320 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r X ( p `  r ) ) ) )  =  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r Z ( p `  r ) ) ) ) )
115102, 114oveq12d 6322 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( (mulGrp `  R )  gsumg  ( r  e.  {
I }  |->  ( r X ( p `  r ) ) ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r X ( p `  r ) ) ) ) )  =  ( ( I X ( p `  I ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r Z ( p `  r ) ) ) ) ) )
11693, 115eqtrd 2464 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `  r ) ) ) )  =  ( ( I X ( p `  I
) )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) ) )
11763, 82, 66, 26, 74, 89, 92gsummptfidmsplit 17560 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) )  =  ( ( (mulGrp `  R )  gsumg  ( r  e.  {
I }  |->  ( r Z ( p `  r ) ) ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r Z ( p `  r ) ) ) ) ) )
11898, 99oveq12d 6322 . . . . . . . . . . . . 13  |-  ( r  =  I  ->  (
r Z ( p `
 r ) )  =  ( I Z ( p `  I
) ) )
11963, 118gsumsn 17584 . . . . . . . . . . . 12  |-  ( ( (mulGrp `  R )  e.  Mnd  /\  I  e.  N  /\  ( I Z ( p `  I ) )  e.  K )  ->  (
(mulGrp `  R )  gsumg  ( r  e.  { I }  |->  ( r Z ( p `  r
) ) ) )  =  ( I Z ( p `  I
) ) )
12095, 5, 61, 119syl3anc 1265 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  {
I }  |->  ( r Z ( p `  r ) ) ) )  =  ( I Z ( p `  I ) ) )
121120oveq1d 6319 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( (mulGrp `  R )  gsumg  ( r  e.  {
I }  |->  ( r Z ( p `  r ) ) ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r Z ( p `  r ) ) ) ) )  =  ( ( I Z ( p `  I ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r Z ( p `  r ) ) ) ) ) )
122117, 121eqtrd 2464 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) )  =  ( ( I Z ( p `  I
) )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  ( N 
\  { I }
)  |->  ( r Z ( p `  r
) ) ) ) ) )
123122oveq2d 6320 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( Y  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) )  =  ( Y  .x.  (
( I Z ( p `  I ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  ( N  \  { I } )  |->  ( r Z ( p `  r ) ) ) ) ) ) )
12481, 116, 1233eqtr4d 2474 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `  r ) ) ) )  =  ( Y  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) )
125124oveq2d 6320 . . . . . 6  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `
 r ) ) ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  .x.  ( Y  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) )
12657adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  R  e.  CRing )
127 zrhpsgnmhm 19148 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  N  e.  Fin )  ->  (
( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
12859, 25, 127syl2anc 666 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
1299, 63mhmf 16584 . . . . . . . . . . 11  |-  ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
) : ( Base `  ( SymGrp `  N )
) --> K )
130128, 129syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) : ( Base `  ( SymGrp `
 N ) ) --> K )
131130ffvelrnda 6036 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  e.  K )
13232, 78crngcom 17792 . . . . . . . . 9  |-  ( ( R  e.  CRing  /\  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  e.  K  /\  Y  e.  K
)  ->  ( (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  Y
)  =  ( Y 
.x.  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
) )
133126, 131, 30, 132syl3anc 1265 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  Y
)  =  ( Y 
.x.  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
) )
134133oveq1d 6319 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  Y
)  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) )  =  ( ( Y 
.x.  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
)  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) )
13574ralrimiva 2840 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  A. r  e.  N  ( r Z ( p `  r ) )  e.  K )
13663, 66, 26, 135gsummptcl 17596 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) )  e.  K )
13732, 78ringass 17794 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  e.  K  /\  Y  e.  K  /\  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) )  e.  K ) )  -> 
( ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  Y
)  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) )  =  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  ( Y  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) ) )
13860, 131, 30, 136, 137syl13anc 1267 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  Y
)  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) )  =  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  ( Y  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) ) )
13932, 78ringass 17794 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  ( Y  e.  K  /\  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  e.  K  /\  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) )  e.  K ) )  -> 
( ( Y  .x.  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) )  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) )  =  ( Y  .x.  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) )
14060, 30, 131, 136, 139syl13anc 1267 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( Y 
.x.  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
)  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) )  =  ( Y  .x.  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  .x.  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) ) )
141134, 138, 1403eqtr3d 2472 . . . . . 6  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  ( Y  .x.  ( (mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) )  =  ( Y 
.x.  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) )
142125, 141eqtrd 2464 . . . . 5  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `
 r ) ) ) ) )  =  ( Y  .x.  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) )
143142mpteq2dva 4509 . . . 4  |-  ( ph  ->  ( p  e.  (
Base `  ( SymGrp `  N ) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `
 r ) ) ) ) ) )  =  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( Y  .x.  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) ) )
144143oveq2d 6320 . . 3  |-  ( ph  ->  ( R  gsumg  ( p  e.  (
Base `  ( SymGrp `  N ) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `
 r ) ) ) ) ) ) )  =  ( R 
gsumg  ( p  e.  ( Base `  ( SymGrp `  N
) )  |->  ( Y 
.x.  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) ) ) )
145 eqid 2423 . . . 4  |-  ( 0g
`  R )  =  ( 0g `  R
)
146 eqid 2423 . . . 4  |-  ( +g  `  R )  =  ( +g  `  R )
1478, 9symgbasfi 17024 . . . . 5  |-  ( N  e.  Fin  ->  ( Base `  ( SymGrp `  N
) )  e.  Fin )
14825, 147syl 17 . . . 4  |-  ( ph  ->  ( Base `  ( SymGrp `
 N ) )  e.  Fin )
14932, 78ringcl 17791 . . . . 5  |-  ( ( R  e.  Ring  /\  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  e.  K  /\  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) )  e.  K )  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) )  e.  K )
15060, 131, 136, 149syl3anc 1265 . . . 4  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) )  e.  K )
151 eqid 2423 . . . . 5  |-  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  .x.  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) )  =  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  .x.  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) )
152 ovex 6332 . . . . . 6  |-  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) )  e. 
_V
153152a1i 11 . . . . 5  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) )  e. 
_V )
154 fvex 5890 . . . . . 6  |-  ( 0g
`  R )  e. 
_V
155154a1i 11 . . . . 5  |-  ( ph  ->  ( 0g `  R
)  e.  _V )
156151, 148, 153, 155fsuppmptdm 7902 . . . 4  |-  ( ph  ->  ( p  e.  (
Base `  ( SymGrp `  N ) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) finSupp 
( 0g `  R
) )
15732, 145, 146, 78, 59, 148, 29, 150, 156gsummulc2 17832 . . 3  |-  ( ph  ->  ( R  gsumg  ( p  e.  (
Base `  ( SymGrp `  N ) )  |->  ( Y  .x.  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) ) )  =  ( Y  .x.  ( R 
gsumg  ( p  e.  ( Base `  ( SymGrp `  N
) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) ) ) )
158144, 157eqtrd 2464 . 2  |-  ( ph  ->  ( R  gsumg  ( p  e.  (
Base `  ( SymGrp `  N ) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `
 r ) ) ) ) ) ) )  =  ( Y 
.x.  ( R  gsumg  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  .x.  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) ) ) ) )
159 mdetrsca.d . . . 4  |-  D  =  ( N maDet  R )
160 eqid 2423 . . . 4  |-  ( ZRHom `  R )  =  ( ZRHom `  R )
161 eqid 2423 . . . 4  |-  (pmSgn `  N )  =  (pmSgn `  N )
162159, 21, 22, 9, 160, 161, 78, 62mdetleib2 19609 . . 3  |-  ( ( R  e.  CRing  /\  X  e.  B )  ->  ( D `  X )  =  ( R  gsumg  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  .x.  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r X ( p `  r ) ) ) ) ) ) ) )
16357, 20, 162syl2anc 666 . 2  |-  ( ph  ->  ( D `  X
)  =  ( R 
gsumg  ( p  e.  ( Base `  ( SymGrp `  N
) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r X ( p `
 r ) ) ) ) ) ) ) )
164159, 21, 22, 9, 160, 161, 78, 62mdetleib2 19609 . . . 4  |-  ( ( R  e.  CRing  /\  Z  e.  B )  ->  ( D `  Z )  =  ( R  gsumg  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  .x.  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) ) ) )
16557, 31, 164syl2anc 666 . . 3  |-  ( ph  ->  ( D `  Z
)  =  ( R 
gsumg  ( p  e.  ( Base `  ( SymGrp `  N
) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  .x.  (
(mulGrp `  R )  gsumg  ( r  e.  N  |->  ( r Z ( p `
 r ) ) ) ) ) ) ) )
166165oveq2d 6320 . 2  |-  ( ph  ->  ( Y  .x.  ( D `  Z )
)  =  ( Y 
.x.  ( R  gsumg  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  .x.  ( (mulGrp `  R
)  gsumg  ( r  e.  N  |->  ( r Z ( p `  r ) ) ) ) ) ) ) ) )
167158, 163, 1663eqtr4d 2474 1  |-  ( ph  ->  ( D `  X
)  =  ( Y 
.x.  ( D `  Z ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1438    e. wcel 1869   _Vcvv 3082    \ cdif 3435    u. cun 3436    i^i cin 3437    C_ wss 3438   (/)c0 3763   {csn 3998   <.cop 4004    |-> cmpt 4481    X. cxp 4850    |` cres 4854    o. ccom 4856    Fn wfn 5595   -->wf 5596   -1-1-onto->wf1o 5599   ` cfv 5600  (class class class)co 6304    oFcof 6542    ^m cmap 7482   Fincfn 7579   Basecbs 15118   +g cplusg 15187   .rcmulr 15188   0gc0g 15335    gsumg cgsu 15336   Mndcmnd 16532   MndHom cmhm 16577   SymGrpcsymg 17015  pmSgncpsgn 17127  CMndccmn 17427  mulGrpcmgp 17720   Ringcrg 17777   CRingccrg 17778   ZRHomczrh 19067   Mat cmat 19428   maDet cmdat 19605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4535  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596  ax-inf2 8154  ax-cnex 9601  ax-resscn 9602  ax-1cn 9603  ax-icn 9604  ax-addcl 9605  ax-addrcl 9606  ax-mulcl 9607  ax-mulrcl 9608  ax-mulcom 9609  ax-addass 9610  ax-mulass 9611  ax-distr 9612  ax-i2m1 9613  ax-1ne0 9614  ax-1rid 9615  ax-rnegex 9616  ax-rrecex 9617  ax-cnre 9618  ax-pre-lttri 9619  ax-pre-lttrn 9620  ax-pre-ltadd 9621  ax-pre-mulgt0 9622  ax-addf 9624  ax-mulf 9625
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-xor 1402  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3302  df-csb 3398  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-pss 3454  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-ot 4007  df-uni 4219  df-int 4255  df-iun 4300  df-iin 4301  df-br 4423  df-opab 4482  df-mpt 4483  df-tr 4518  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6266  df-ov 6307  df-oprab 6308  df-mpt2 6309  df-of 6544  df-om 6706  df-1st 6806  df-2nd 6807  df-supp 6925  df-tpos 6983  df-wrecs 7038  df-recs 7100  df-rdg 7138  df-1o 7192  df-2o 7193  df-oadd 7196  df-er 7373  df-map 7484  df-pm 7485  df-ixp 7533  df-en 7580  df-dom 7581  df-sdom 7582  df-fin 7583  df-fsupp 7892  df-sup 7964  df-oi 8033  df-card 8380  df-cda 8604  df-pnf 9683  df-mnf 9684  df-xr 9685  df-ltxr 9686  df-le 9687  df-sub 9868  df-neg 9869  df-div 10276  df-nn 10616  df-2 10674  df-3 10675  df-4 10676  df-5 10677  df-6 10678  df-7 10679  df-8 10680  df-9 10681  df-10 10682  df-n0 10876  df-z 10944  df-dec 11058  df-uz 11166  df-rp 11309  df-fz 11791  df-fzo 11922  df-seq 12219  df-exp 12278  df-hash 12521  df-word 12666  df-lsw 12667  df-concat 12668  df-s1 12669  df-substr 12670  df-splice 12671  df-reverse 12672  df-s2 12944  df-struct 15120  df-ndx 15121  df-slot 15122  df-base 15123  df-sets 15124  df-ress 15125  df-plusg 15200  df-mulr 15201  df-starv 15202  df-sca 15203  df-vsca 15204  df-ip 15205  df-tset 15206  df-ple 15207  df-ds 15209  df-unif 15210  df-hom 15211  df-cco 15212  df-0g 15337  df-gsum 15338  df-prds 15343  df-pws 15345  df-mre 15489  df-mrc 15490  df-acs 15492  df-mgm 16485  df-sgrp 16524  df-mnd 16534  df-mhm 16579  df-submnd 16580  df-grp 16670  df-minusg 16671  df-mulg 16673  df-subg 16811  df-ghm 16878  df-gim 16920  df-cntz 16968  df-oppg 16994  df-symg 17016  df-pmtr 17080  df-psgn 17129  df-cmn 17429  df-abl 17430  df-mgp 17721  df-ur 17733  df-ring 17779  df-cring 17780  df-oppr 17848  df-dvdsr 17866  df-unit 17867  df-invr 17897  df-dvr 17908  df-rnghom 17940  df-drng 17974  df-subrg 18003  df-sra 18392  df-rgmod 18393  df-cnfld 18968  df-zring 19036  df-zrh 19071  df-dsmm 19291  df-frlm 19306  df-mat 19429  df-mdet 19606
This theorem is referenced by:  mdetrsca2  19625  mdetuni0  19642  mdetmul  19644  smadiadetg  19694
  Copyright terms: Public domain W3C validator