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 ffvelrnd 
 |-  ( ( 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 fnssres 
 |-  ( ( Z Fn ( N X. N ) /\ ( { I } X. N ) C_ ( N X. N ) ) -> ( Z |` ( { I } X. N ) ) Fn ( { I } X. N ) )
45 40 43 44 syl2anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Z |` ( { I } X. N ) ) Fn ( { I } X. N ) )
46 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 ) >. ) )
47 34 35 45 46 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 ) >. ) ) )
48 27 47 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 ) >. ) ) )
49 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 ) >. )
50 df-ov 
 |-  ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( ( Z |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. )
51 50 oveq2i 
 |-  ( Y .x. ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) = ( Y .x. ( ( Z |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. ) )
52 48 49 51 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 ) ) ) )
53 14 26 52 3eqtr3d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I X ( p ` I ) ) = ( Y .x. ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) )
54 ovres 
 |-  ( ( I e. { I } /\ ( p ` I ) e. N ) -> ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( I Z ( p ` I ) ) )
55 17 24 54 syl2anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( I Z ( p ` I ) ) )
56 55 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Y .x. ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) = ( Y .x. ( I Z ( p ` I ) ) ) )
57 53 56 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I X ( p ` I ) ) = ( Y .x. ( I Z ( p ` I ) ) ) )
58 57 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 ) ) ) ) ) )
59 crngring 
 |-  ( R e. CRing -> R e. Ring )
60 6 59 syl 
 |-  ( ph -> R e. Ring )
61 60 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> R e. Ring )
62 39 15 24 fovrnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I Z ( p ` I ) ) e. K )
63 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
64 63 4 mgpbas 
 |-  K = ( Base ` ( mulGrp ` R ) )
65 63 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
66 6 65 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
67 66 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( mulGrp ` R ) e. CMnd )
68 difssd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( N \ { I } ) C_ N )
69 32 68 ssfid 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( N \ { I } ) e. Fin )
70 eldifi 
 |-  ( r e. ( N \ { I } ) -> r e. N )
71 38 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> Z : ( N X. N ) --> K )
72 simpr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> r e. N )
73 23 ffvelrnda 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( p ` r ) e. N )
74 71 72 73 fovrnd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( r Z ( p ` r ) ) e. K )
75 70 74 sylan2 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r Z ( p ` r ) ) e. K )
76 75 ralrimiva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. r e. ( N \ { I } ) ( r Z ( p ` r ) ) e. K )
77 64 67 69 76 gsummptcl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) e. K )
78 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 ) ) ) ) ) ) )
79 61 35 62 77 78 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 ) ) ) ) ) ) )
80 58 79 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 ) ) ) ) ) ) )
81 63 5 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
82 2 4 3 matbas2i 
 |-  ( X e. B -> X e. ( K ^m ( N X. N ) ) )
83 elmapi 
 |-  ( X e. ( K ^m ( N X. N ) ) -> X : ( N X. N ) --> K )
84 7 82 83 3syl 
 |-  ( ph -> X : ( N X. N ) --> K )
85 84 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> X : ( N X. N ) --> K )
86 85 72 73 fovrnd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( r X ( p ` r ) ) e. K )
87 disjdif 
 |-  ( { I } i^i ( N \ { I } ) ) = (/)
88 87 a1i 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } i^i ( N \ { I } ) ) = (/) )
89 undif 
 |-  ( { I } C_ N <-> ( { I } u. ( N \ { I } ) ) = N )
90 41 89 sylib 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } u. ( N \ { I } ) ) = N )
91 90 eqcomd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> N = ( { I } u. ( N \ { I } ) ) )
92 64 81 67 32 86 88 91 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 ) ) ) ) ) )
93 cmnmnd 
 |-  ( ( mulGrp ` R ) e. CMnd -> ( mulGrp ` R ) e. Mnd )
94 67 93 syl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( mulGrp ` R ) e. Mnd )
95 84 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> X : ( N X. N ) --> K )
96 95 15 24 fovrnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I X ( p ` I ) ) e. K )
97 id 
 |-  ( r = I -> r = I )
98 fveq2 
 |-  ( r = I -> ( p ` r ) = ( p ` I ) )
99 97 98 oveq12d 
 |-  ( r = I -> ( r X ( p ` r ) ) = ( I X ( p ` I ) ) )
100 64 99 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 ) ) )
101 94 15 96 100 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) = ( I X ( p ` I ) ) )
102 12 oveqd 
 |-  ( ph -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r ( Z |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) )
103 102 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 ) ) )
104 simpr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> r e. ( N \ { I } ) )
105 70 73 sylan2 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( p ` r ) e. N )
106 ovres 
 |-  ( ( r e. ( N \ { I } ) /\ ( p ` r ) e. N ) -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r X ( p ` r ) ) )
107 104 105 106 syl2anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r X ( p ` r ) ) )
108 ovres 
 |-  ( ( r e. ( N \ { I } ) /\ ( p ` r ) e. N ) -> ( r ( Z |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r Z ( p ` r ) ) )
109 104 105 108 syl2anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r ( Z |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r Z ( p ` r ) ) )
110 103 107 109 3eqtr3d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r X ( p ` r ) ) = ( r Z ( p ` r ) ) )
111 110 mpteq2dva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) = ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) )
112 111 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 ) ) ) ) )
113 101 112 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 ) ) ) ) ) )
114 92 113 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 ) ) ) ) ) )
115 64 81 67 32 74 88 91 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 ) ) ) ) ) )
116 97 98 oveq12d 
 |-  ( r = I -> ( r Z ( p ` r ) ) = ( I Z ( p ` I ) ) )
117 64 116 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 ) ) )
118 94 15 62 117 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) = ( I Z ( p ` I ) ) )
119 118 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 ) ) ) ) ) )
120 115 119 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 ) ) ) ) ) )
121 120 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 ) ) ) ) ) ) )
122 80 114 121 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 ) ) ) ) ) )
123 122 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 ) ) ) ) ) ) )
124 6 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> R e. CRing )
125 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
126 60 31 125 syl2anc 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
127 19 64 mhmf 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
128 126 127 syl 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
129 128 ffvelrnda 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. K )
130 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 ) ) )
131 124 129 35 130 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. Y ) = ( Y .x. ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ) )
132 131 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 ) ) ) ) ) )
133 74 ralrimiva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. r e. N ( r Z ( p ` r ) ) e. K )
134 64 67 32 133 gsummptcl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) e. K )
135 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 ) ) ) ) ) ) )
136 61 129 35 134 135 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 ) ) ) ) ) ) )
137 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 ) ) ) ) ) ) )
138 61 35 129 134 137 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 ) ) ) ) ) ) )
139 132 136 138 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 ) ) ) ) ) ) )
140 123 139 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 ) ) ) ) ) ) )
141 140 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 ) ) ) ) ) ) ) )
142 141 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 ) ) ) ) ) ) ) ) )
143 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
144 eqid 
 |-  ( +g ` R ) = ( +g ` R )
145 18 19 symgbasfi 
 |-  ( N e. Fin -> ( Base ` ( SymGrp ` N ) ) e. Fin )
146 31 145 syl 
 |-  ( ph -> ( Base ` ( SymGrp ` N ) ) e. Fin )
147 4 5 ringcl 
 |-  ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. K /\ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) e. K ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) .x. ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) e. K )
148 61 129 134 147 syl3anc 
 |-  ( ( 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 )
149 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 ) ) ) ) ) )
150 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 )
151 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
152 149 146 150 151 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 ) )
153 4 143 144 5 60 146 8 148 152 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 ) ) ) ) ) ) ) ) )
154 142 153 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 ) ) ) ) ) ) ) ) )
155 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
156 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
157 1 2 3 19 155 156 5 63 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 ) ) ) ) ) ) ) )
158 6 7 157 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 ) ) ) ) ) ) ) )
159 1 2 3 19 155 156 5 63 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 ) ) ) ) ) ) ) )
160 6 9 159 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 ) ) ) ) ) ) ) )
161 160 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 ) ) ) ) ) ) ) ) )
162 154 158 161 3eqtr4d 
 |-  ( ph -> ( D ` X ) = ( Y .x. ( D ` Z ) ) )