Metamath Proof Explorer

Theorem mdetrsca

Description: The determinant function is homogeneous for each row: If the matrices X and Z are identical except for the I -th row, and the I -th row of the matrix X is the componentwise product of the I -th row of the matrix Z and the scalar Y , then 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)

Ref Expression
Hypotheses 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 mdetrsca 
|- ( ph -> ( D ` X ) = ( Y .x. ( D ` Z ) ) )

Proof

Step Hyp Ref Expression
1 mdetrsca.d 
 |-  D = ( N maDet R )
2 mdetrsca.a 
 |-  A = ( N Mat R )
3 mdetrsca.b 
 |-  B = ( Base ` A )
4 mdetrsca.k 
 |-  K = ( Base ` R )
5 mdetrsca.t 
 |-  .x. = ( .r ` R )
6 mdetrsca.r 
 |-  ( ph -> R e. CRing )
7 mdetrsca.x 
 |-  ( ph -> X e. B )
8 mdetrsca.y 
 |-  ( ph -> Y e. K )
9 mdetrsca.z 
 |-  ( ph -> Z e. B )
10 mdetrsca.i 
 |-  ( ph -> I e. N )
11 mdetrsca.eq 
 |-  ( ph -> ( X |` ( { I } X. N ) ) = ( ( ( { I } X. N ) X. { Y } ) oF .x. ( Z |` ( { I } X. N ) ) ) )
12 mdetrsca.ne 
 |-  ( ph -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Z |` ( ( N \ { I } ) X. N ) ) )
13 11 oveqd 
 |-  ( ph -> ( I ( X |` ( { I } X. N ) ) ( p ` I ) ) = ( I ( ( ( { I } X. N ) X. { Y } ) oF .x. ( Z |` ( { I } X. N ) ) ) ( p ` I ) ) )
14 13 adantr 
 |-  ( ( 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 ) ) )
15 10 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> I e. N )
16 snidg 
 |-  ( I e. N -> I e. { I } )
17 15 16 syl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> I e. { I } )
18 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
19 eqid 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
20 18 19 symgbasf1o 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) -> p : N -1-1-onto-> N )
21 20 adantl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> p : N -1-1-onto-> N )
22 f1of 
 |-  ( p : N -1-1-onto-> N -> p : N --> N )
23 21 22 syl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> p : N --> N )
24 23 15 ffvelcdmd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( p ` I ) e. N )
25 ovres 
 |-  ( ( I e. { I } /\ ( p ` I ) e. N ) -> ( I ( X |` ( { I } X. N ) ) ( p ` I ) ) = ( I X ( p ` I ) ) )
26 17 24 25 syl2anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( X |` ( { I } X. N ) ) ( p ` I ) ) = ( I X ( p ` I ) ) )
27 17 24 opelxpd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> <. I , ( p ` I ) >. e. ( { I } X. N ) )
28 snfi 
 |-  { I } e. Fin
29 2 3 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
30 7 29 syl 
 |-  ( ph -> ( N e. Fin /\ R e. _V ) )
31 30 simpld 
 |-  ( ph -> N e. Fin )
32 31 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> N e. Fin )
33 xpfi 
 |-  ( ( { I } e. Fin /\ N e. Fin ) -> ( { I } X. N ) e. Fin )
34 28 32 33 sylancr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } X. N ) e. Fin )
35 8 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> Y e. K )
36 2 4 3 matbas2i 
 |-  ( Z e. B -> Z e. ( K ^m ( N X. N ) ) )
37 elmapi 
 |-  ( Z e. ( K ^m ( N X. N ) ) -> Z : ( N X. N ) --> K )
38 9 36 37 3syl 
 |-  ( ph -> Z : ( N X. N ) --> K )
39 38 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> Z : ( N X. N ) --> K )
40 39 ffnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> Z Fn ( N X. N ) )
41 15 snssd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> { I } C_ N )
42 xpss1 
 |-  ( { I } C_ N -> ( { I } X. N ) C_ ( N X. N ) )
43 41 42 syl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } X. N ) C_ ( N X. N ) )
44 40 43 fnssresd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Z |` ( { I } X. N ) ) Fn ( { I } X. N ) )
45 eqidd 
 |-  ( ( ( 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 ) >. ) )
46 34 35 44 45 ofc1 
 |-  ( ( ( 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 ) >. ) ) )
47 27 46 mpdan 
 |-  ( ( 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 ) >. ) ) )
48 df-ov 
 |-  ( 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 ) >. )
49 df-ov 
 |-  ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( ( Z |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. )
50 49 oveq2i 
 |-  ( Y .x. ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) = ( Y .x. ( ( Z |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. ) )
51 47 48 50 3eqtr4g 
 |-  ( ( 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 ) ) ) )
52 14 26 51 3eqtr3d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I X ( p ` I ) ) = ( Y .x. ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) )
53 ovres 
 |-  ( ( I e. { I } /\ ( p ` I ) e. N ) -> ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( I Z ( p ` I ) ) )
54 17 24 53 syl2anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( I Z ( p ` I ) ) )
55 54 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Y .x. ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) = ( Y .x. ( I Z ( p ` I ) ) ) )
56 52 55 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I X ( p ` I ) ) = ( Y .x. ( I Z ( p ` I ) ) ) )
57 56 oveq1d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( I X ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) = ( ( Y .x. ( I Z ( p ` I ) ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) )
58 6 crngringd 
 |-  ( ph -> R e. Ring )
59 58 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> R e. Ring )
60 39 15 24 fovcdmd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I Z ( p ` I ) ) e. K )
61 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
62 61 4 mgpbas 
 |-  K = ( Base ` ( mulGrp ` R ) )
63 61 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
64 6 63 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
65 64 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( mulGrp ` R ) e. CMnd )
66 difssd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( N \ { I } ) C_ N )
67 32 66 ssfid 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( N \ { I } ) e. Fin )
68 eldifi 
 |-  ( r e. ( N \ { I } ) -> r e. N )
69 38 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> Z : ( N X. N ) --> K )
70 simpr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> r e. N )
71 23 ffvelcdmda 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( p ` r ) e. N )
72 69 70 71 fovcdmd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( r Z ( p ` r ) ) e. K )
73 68 72 sylan2 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r Z ( p ` r ) ) e. K )
74 73 ralrimiva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. r e. ( N \ { I } ) ( r Z ( p ` r ) ) e. K )
75 62 65 67 74 gsummptcl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) e. K )
76 4 5 ringass 
 |-  ( ( R e. Ring /\ ( Y e. K /\ ( I Z ( p ` I ) ) e. K /\ ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) e. K ) ) -> ( ( Y .x. ( I Z ( p ` I ) ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) = ( Y .x. ( ( I Z ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) ) )
77 59 35 60 75 76 syl13anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( Y .x. ( I Z ( p ` I ) ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) = ( Y .x. ( ( I Z ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) ) )
78 57 77 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( I X ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) = ( Y .x. ( ( I Z ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) ) )
79 61 5 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
80 2 4 3 matbas2i 
 |-  ( X e. B -> X e. ( K ^m ( N X. N ) ) )
81 elmapi 
 |-  ( X e. ( K ^m ( N X. N ) ) -> X : ( N X. N ) --> K )
82 7 80 81 3syl 
 |-  ( ph -> X : ( N X. N ) --> K )
83 82 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> X : ( N X. N ) --> K )
84 83 70 71 fovcdmd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( r X ( p ` r ) ) e. K )
85 disjdif 
 |-  ( { I } i^i ( N \ { I } ) ) = (/)
86 85 a1i 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } i^i ( N \ { I } ) ) = (/) )
87 undif 
 |-  ( { I } C_ N <-> ( { I } u. ( N \ { I } ) ) = N )
88 41 87 sylib 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } u. ( N \ { I } ) ) = N )
89 88 eqcomd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> N = ( { I } u. ( N \ { I } ) ) )
90 62 79 65 32 84 86 89 gsummptfidmsplit 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) )
91 65 cmnmndd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( mulGrp ` R ) e. Mnd )
92 82 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> X : ( N X. N ) --> K )
93 92 15 24 fovcdmd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I X ( p ` I ) ) e. K )
94 id 
 |-  ( r = I -> r = I )
95 fveq2 
 |-  ( r = I -> ( p ` r ) = ( p ` I ) )
96 94 95 oveq12d 
 |-  ( r = I -> ( r X ( p ` r ) ) = ( I X ( p ` I ) ) )
97 62 96 gsumsn 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ I e. N /\ ( I X ( p ` I ) ) e. K ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) = ( I X ( p ` I ) ) )
98 91 15 93 97 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) = ( I X ( p ` I ) ) )
99 12 oveqd 
 |-  ( ph -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r ( Z |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) )
100 99 ad2antrr 
 |-  ( ( ( 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 ) ) )
101 simpr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> r e. ( N \ { I } ) )
102 68 71 sylan2 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( p ` r ) e. N )
103 ovres 
 |-  ( ( r e. ( N \ { I } ) /\ ( p ` r ) e. N ) -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r X ( p ` r ) ) )
104 101 102 103 syl2anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r X ( p ` r ) ) )
105 ovres 
 |-  ( ( r e. ( N \ { I } ) /\ ( p ` r ) e. N ) -> ( r ( Z |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r Z ( p ` r ) ) )
106 101 102 105 syl2anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r ( Z |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r Z ( p ` r ) ) )
107 100 104 106 3eqtr3d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r X ( p ` r ) ) = ( r Z ( p ` r ) ) )
108 107 mpteq2dva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) = ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) )
109 108 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) = ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) )
110 98 109 oveq12d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) = ( ( I X ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) )
111 90 110 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) = ( ( I X ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) )
112 62 79 65 32 72 86 89 gsummptfidmsplit 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) )
113 94 95 oveq12d 
 |-  ( r = I -> ( r Z ( p ` r ) ) = ( I Z ( p ` I ) ) )
114 62 113 gsumsn 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ I e. N /\ ( I Z ( p ` I ) ) e. K ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) = ( I Z ( p ` I ) ) )
115 91 15 60 114 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) = ( I Z ( p ` I ) ) )
116 115 oveq1d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) = ( ( I Z ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) )
117 112 116 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) = ( ( I Z ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) )
118 117 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Y .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) = ( Y .x. ( ( I Z ( p ` I ) ) .x. ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) ) )
119 78 111 118 3eqtr4d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) = ( Y .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) )
120 119 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( Y .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
121 6 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> R e. CRing )
122 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
123 58 31 122 syl2anc 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
124 19 62 mhmf 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
125 123 124 syl 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
126 125 ffvelcdmda 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. K )
127 4 5 crngcom 
 |-  ( ( 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 ) ) )
128 121 126 35 127 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. Y ) = ( Y .x. ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ) )
129 128 oveq1d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. Y ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) = ( ( Y .x. ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) )
130 72 ralrimiva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. r e. N ( r Z ( p ` r ) ) e. K )
131 62 65 32 130 gsummptcl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) e. K )
132 4 5 ringass 
 |-  ( ( R e. Ring /\ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. K /\ Y e. K /\ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) e. K ) ) -> ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. Y ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( Y .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
133 59 126 35 131 132 syl13anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. Y ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( Y .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
134 4 5 ringass 
 |-  ( ( R e. Ring /\ ( Y e. K /\ ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. K /\ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) e. K ) ) -> ( ( Y .x. ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) = ( Y .x. ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
135 59 35 126 131 134 syl13anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( Y .x. ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) = ( Y .x. ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
136 129 133 135 3eqtr3d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( Y .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) = ( Y .x. ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
137 120 136 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) = ( Y .x. ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
138 137 mpteq2dva 
 |-  ( ph -> ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( Y .x. ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) )
139 138 oveq2d 
 |-  ( ph -> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( Y .x. ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) )
140 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
141 18 19 symgbasfi 
 |-  ( N e. Fin -> ( Base ` ( SymGrp ` N ) ) e. Fin )
142 31 141 syl 
 |-  ( ph -> ( Base ` ( SymGrp ` N ) ) e. Fin )
143 4 5 59 126 131 ringcld 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) e. K )
144 eqid 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) )
145 ovexd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) e. _V )
146 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
147 144 142 145 146 fsuppmptdm 
 |-  ( ph -> ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) finSupp ( 0g ` R ) )
148 4 140 5 58 142 8 143 147 gsummulc2 
 |-  ( ph -> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( Y .x. ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) = ( Y .x. ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) )
149 139 148 eqtrd 
 |-  ( ph -> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) ) = ( Y .x. ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) )
150 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
151 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
152 1 2 3 19 150 151 5 61 mdetleib2 
 |-  ( ( R e. CRing /\ X e. B ) -> ( D ` X ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) ) )
153 6 7 152 syl2anc 
 |-  ( ph -> ( D ` X ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) ) )
154 1 2 3 19 150 151 5 61 mdetleib2 
 |-  ( ( R e. CRing /\ Z e. B ) -> ( D ` Z ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) )
155 6 9 154 syl2anc 
 |-  ( ph -> ( D ` Z ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) )
156 155 oveq2d 
 |-  ( ph -> ( Y .x. ( D ` Z ) ) = ( Y .x. ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) )
157 149 153 156 3eqtr4d 
 |-  ( ph -> ( D ` X ) = ( Y .x. ( D ` Z ) ) )