Metamath Proof Explorer

Theorem mdetrlin

Description: The determinant function is additive for each row: The matrices X, Y, Z are identical except for the I's row, and the I's row of the matrix X is the componentwise sum of the I's row of the matrices Y and Z. In this case the determinant of X is the sum of the determinants of Y and Z. (Contributed by SO, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses mdetrlin.d 
|- D = ( N maDet R )
mdetrlin.a 
|- A = ( N Mat R )
mdetrlin.b 
|- B = ( Base ` A )
mdetrlin.p 
|- .+ = ( +g ` R )
mdetrlin.r 
|- ( ph -> R e. CRing )
mdetrlin.x 
|- ( ph -> X e. B )
mdetrlin.y 
|- ( ph -> Y e. B )
mdetrlin.z 
|- ( ph -> Z e. B )
mdetrlin.i 
|- ( ph -> I e. N )
mdetrlin.eq 
|- ( ph -> ( X |` ( { I } X. N ) ) = ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) )
mdetrlin.ne1 
|- ( ph -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Y |` ( ( N \ { I } ) X. N ) ) )
mdetrlin.ne2 
|- ( ph -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Z |` ( ( N \ { I } ) X. N ) ) )
Assertion mdetrlin 
|- ( ph -> ( D ` X ) = ( ( D ` Y ) .+ ( D ` Z ) ) )

Proof

Step Hyp Ref Expression
1 mdetrlin.d 
 |-  D = ( N maDet R )
2 mdetrlin.a 
 |-  A = ( N Mat R )
3 mdetrlin.b 
 |-  B = ( Base ` A )
4 mdetrlin.p 
 |-  .+ = ( +g ` R )
5 mdetrlin.r 
 |-  ( ph -> R e. CRing )
6 mdetrlin.x 
 |-  ( ph -> X e. B )
7 mdetrlin.y 
 |-  ( ph -> Y e. B )
8 mdetrlin.z 
 |-  ( ph -> Z e. B )
9 mdetrlin.i 
 |-  ( ph -> I e. N )
10 mdetrlin.eq 
 |-  ( ph -> ( X |` ( { I } X. N ) ) = ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) )
11 mdetrlin.ne1 
 |-  ( ph -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Y |` ( ( N \ { I } ) X. N ) ) )
12 mdetrlin.ne2 
 |-  ( ph -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Z |` ( ( N \ { I } ) X. N ) ) )
13 fvex 
 |-  ( Base ` ( SymGrp ` N ) ) e. _V
14 ovex 
 |-  ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) e. _V
15 eqid 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) )
16 14 15 fnmpti 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) Fn ( Base ` ( SymGrp ` N ) )
17 ovex 
 |-  ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) e. _V
18 eqid 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) )
19 17 18 fnmpti 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) Fn ( Base ` ( SymGrp ` N ) )
20 ofmpteq 
 |-  ( ( ( Base ` ( SymGrp ` N ) ) e. _V /\ ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) Fn ( Base ` ( SymGrp ` N ) ) /\ ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) Fn ( Base ` ( SymGrp ` N ) ) ) -> ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) oF .+ ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) .+ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) )
21 13 16 19 20 mp3an 
 |-  ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) oF .+ ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) .+ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
22 crngring 
 |-  ( R e. CRing -> R e. Ring )
23 5 22 syl 
 |-  ( ph -> R e. Ring )
24 23 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> R e. Ring )
25 2 3 matrcl 
 |-  ( Y e. B -> ( N e. Fin /\ R e. _V ) )
26 7 25 syl 
 |-  ( ph -> ( N e. Fin /\ R e. _V ) )
27 26 simpld 
 |-  ( ph -> N e. Fin )
28 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
29 23 27 28 syl2anc 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
30 eqid 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
31 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
32 eqid 
 |-  ( Base ` R ) = ( Base ` R )
33 31 32 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
34 30 33 mhmf 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> ( Base ` R ) )
35 29 34 syl 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> ( Base ` R ) )
36 35 ffvelrnda 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. ( Base ` R ) )
37 31 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
38 5 37 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
39 38 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( mulGrp ` R ) e. CMnd )
40 27 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> N e. Fin )
41 2 32 3 matbas2i 
 |-  ( Y e. B -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
42 elmapi 
 |-  ( Y e. ( ( Base ` R ) ^m ( N X. N ) ) -> Y : ( N X. N ) --> ( Base ` R ) )
43 7 41 42 3syl 
 |-  ( ph -> Y : ( N X. N ) --> ( Base ` R ) )
44 43 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> Y : ( N X. N ) --> ( Base ` R ) )
45 simpr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> r e. N )
46 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
47 46 30 symgbasf 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) -> p : N --> N )
48 47 adantl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> p : N --> N )
49 48 ffvelrnda 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( p ` r ) e. N )
50 44 45 49 fovrnd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( r Y ( p ` r ) ) e. ( Base ` R ) )
51 50 ralrimiva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. r e. N ( r Y ( p ` r ) ) e. ( Base ` R ) )
52 33 39 40 51 gsummptcl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) e. ( Base ` R ) )
53 2 32 3 matbas2i 
 |-  ( Z e. B -> Z e. ( ( Base ` R ) ^m ( N X. N ) ) )
54 elmapi 
 |-  ( Z e. ( ( Base ` R ) ^m ( N X. N ) ) -> Z : ( N X. N ) --> ( Base ` R ) )
55 8 53 54 3syl 
 |-  ( ph -> Z : ( N X. N ) --> ( Base ` R ) )
56 55 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> Z : ( N X. N ) --> ( Base ` R ) )
57 56 45 49 fovrnd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( r Z ( p ` r ) ) e. ( Base ` R ) )
58 57 ralrimiva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. r e. N ( r Z ( p ` r ) ) e. ( Base ` R ) )
59 33 39 40 58 gsummptcl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) e. ( Base ` R ) )
60 eqid 
 |-  ( .r ` R ) = ( .r ` R )
61 32 4 60 ringdi 
 |-  ( ( R e. Ring /\ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) e. ( Base ` R ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) = ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) .+ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
62 24 36 52 59 61 syl13anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) = ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) .+ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) )
63 cmnmnd 
 |-  ( ( mulGrp ` R ) e. CMnd -> ( mulGrp ` R ) e. Mnd )
64 39 63 syl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( mulGrp ` R ) e. Mnd )
65 9 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> I e. N )
66 43 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> Y : ( N X. N ) --> ( Base ` R ) )
67 48 65 ffvelrnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( p ` I ) e. N )
68 66 65 67 fovrnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I Y ( p ` I ) ) e. ( Base ` R ) )
69 id 
 |-  ( r = I -> r = I )
70 fveq2 
 |-  ( r = I -> ( p ` r ) = ( p ` I ) )
71 69 70 oveq12d 
 |-  ( r = I -> ( r Y ( p ` r ) ) = ( I Y ( p ` I ) ) )
72 33 71 gsumsn 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ I e. N /\ ( I Y ( p ` I ) ) e. ( Base ` R ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) = ( I Y ( p ` I ) ) )
73 64 65 68 72 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) = ( I Y ( p ` I ) ) )
74 73 68 eqeltrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) e. ( Base ` R ) )
75 55 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> Z : ( N X. N ) --> ( Base ` R ) )
76 75 65 67 fovrnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I Z ( p ` I ) ) e. ( Base ` R ) )
77 69 70 oveq12d 
 |-  ( r = I -> ( r Z ( p ` r ) ) = ( I Z ( p ` I ) ) )
78 33 77 gsumsn 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ I e. N /\ ( I Z ( p ` I ) ) e. ( Base ` R ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) = ( I Z ( p ` I ) ) )
79 64 65 76 78 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) = ( I Z ( p ` I ) ) )
80 79 76 eqeltrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) e. ( Base ` R ) )
81 difssd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( N \ { I } ) C_ N )
82 40 81 ssfid 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( N \ { I } ) e. Fin )
83 eldifi 
 |-  ( r e. ( N \ { I } ) -> r e. N )
84 2 32 3 matbas2i 
 |-  ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
85 elmapi 
 |-  ( X e. ( ( Base ` R ) ^m ( N X. N ) ) -> X : ( N X. N ) --> ( Base ` R ) )
86 6 84 85 3syl 
 |-  ( ph -> X : ( N X. N ) --> ( Base ` R ) )
87 86 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> X : ( N X. N ) --> ( Base ` R ) )
88 87 45 49 fovrnd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. N ) -> ( r X ( p ` r ) ) e. ( Base ` R ) )
89 83 88 sylan2 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r X ( p ` r ) ) e. ( Base ` R ) )
90 89 ralrimiva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. r e. ( N \ { I } ) ( r X ( p ` r ) ) e. ( Base ` R ) )
91 33 39 82 90 gsummptcl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) e. ( Base ` R ) )
92 32 4 60 ringdir 
 |-  ( ( R e. Ring /\ ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) e. ( Base ` R ) ) ) -> ( ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) = ( ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) .+ ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) ) )
93 24 74 80 91 92 syl13anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) = ( ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) .+ ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) ) )
94 31 60 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
95 disjdif 
 |-  ( { I } i^i ( N \ { I } ) ) = (/)
96 95 a1i 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } i^i ( N \ { I } ) ) = (/) )
97 9 snssd 
 |-  ( ph -> { I } C_ N )
98 97 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> { I } C_ N )
99 undif 
 |-  ( { I } C_ N <-> ( { I } u. ( N \ { I } ) ) = N )
100 98 99 sylib 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } u. ( N \ { I } ) ) = N )
101 100 eqcomd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> N = ( { I } u. ( N \ { I } ) ) )
102 33 94 39 40 88 96 101 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 ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) )
103 10 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( X |` ( { I } X. N ) ) = ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) )
104 103 oveqd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( X |` ( { I } X. N ) ) ( p ` I ) ) = ( I ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) ( p ` I ) ) )
105 xpss1 
 |-  ( { I } C_ N -> ( { I } X. N ) C_ ( N X. N ) )
106 98 105 syl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } X. N ) C_ ( N X. N ) )
107 66 106 fssresd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Y |` ( { I } X. N ) ) : ( { I } X. N ) --> ( Base ` R ) )
108 107 ffnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Y |` ( { I } X. N ) ) Fn ( { I } X. N ) )
109 75 106 fssresd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Z |` ( { I } X. N ) ) : ( { I } X. N ) --> ( Base ` R ) )
110 109 ffnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( Z |` ( { I } X. N ) ) Fn ( { I } X. N ) )
111 snex 
 |-  { I } e. _V
112 xpexg 
 |-  ( ( { I } e. _V /\ N e. Fin ) -> ( { I } X. N ) e. _V )
113 111 40 112 sylancr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( { I } X. N ) e. _V )
114 snidg 
 |-  ( I e. N -> I e. { I } )
115 65 114 syl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> I e. { I } )
116 115 67 opelxpd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> <. I , ( p ` I ) >. e. ( { I } X. N ) )
117 fnfvof 
 |-  ( ( ( ( Y |` ( { I } X. N ) ) Fn ( { I } X. N ) /\ ( Z |` ( { I } X. N ) ) Fn ( { I } X. N ) ) /\ ( ( { I } X. N ) e. _V /\ <. I , ( p ` I ) >. e. ( { I } X. N ) ) ) -> ( ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) ` <. I , ( p ` I ) >. ) = ( ( ( Y |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. ) .+ ( ( Z |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. ) ) )
118 108 110 113 116 117 syl22anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) ` <. I , ( p ` I ) >. ) = ( ( ( Y |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. ) .+ ( ( Z |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. ) ) )
119 df-ov 
 |-  ( I ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) ( p ` I ) ) = ( ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) ` <. I , ( p ` I ) >. )
120 df-ov 
 |-  ( I ( Y |` ( { I } X. N ) ) ( p ` I ) ) = ( ( Y |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. )
121 df-ov 
 |-  ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( ( Z |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. )
122 120 121 oveq12i 
 |-  ( ( I ( Y |` ( { I } X. N ) ) ( p ` I ) ) .+ ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) = ( ( ( Y |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. ) .+ ( ( Z |` ( { I } X. N ) ) ` <. I , ( p ` I ) >. ) )
123 118 119 122 3eqtr4g 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) ( p ` I ) ) = ( ( I ( Y |` ( { I } X. N ) ) ( p ` I ) ) .+ ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) )
124 104 123 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( X |` ( { I } X. N ) ) ( p ` I ) ) = ( ( I ( Y |` ( { I } X. N ) ) ( p ` I ) ) .+ ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) )
125 ovres 
 |-  ( ( I e. { I } /\ ( p ` I ) e. N ) -> ( I ( X |` ( { I } X. N ) ) ( p ` I ) ) = ( I X ( p ` I ) ) )
126 115 67 125 syl2anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( X |` ( { I } X. N ) ) ( p ` I ) ) = ( I X ( p ` I ) ) )
127 ovres 
 |-  ( ( I e. { I } /\ ( p ` I ) e. N ) -> ( I ( Y |` ( { I } X. N ) ) ( p ` I ) ) = ( I Y ( p ` I ) ) )
128 115 67 127 syl2anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( Y |` ( { I } X. N ) ) ( p ` I ) ) = ( I Y ( p ` I ) ) )
129 ovres 
 |-  ( ( I e. { I } /\ ( p ` I ) e. N ) -> ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( I Z ( p ` I ) ) )
130 115 67 129 syl2anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) = ( I Z ( p ` I ) ) )
131 128 130 oveq12d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( I ( Y |` ( { I } X. N ) ) ( p ` I ) ) .+ ( I ( Z |` ( { I } X. N ) ) ( p ` I ) ) ) = ( ( I Y ( p ` I ) ) .+ ( I Z ( p ` I ) ) ) )
132 124 126 131 3eqtr3d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I X ( p ` I ) ) = ( ( I Y ( p ` I ) ) .+ ( I Z ( p ` I ) ) ) )
133 86 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> X : ( N X. N ) --> ( Base ` R ) )
134 133 65 67 fovrnd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( I X ( p ` I ) ) e. ( Base ` R ) )
135 69 70 oveq12d 
 |-  ( r = I -> ( r X ( p ` r ) ) = ( I X ( p ` I ) ) )
136 33 135 gsumsn 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ I e. N /\ ( I X ( p ` I ) ) e. ( Base ` R ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) = ( I X ( p ` I ) ) )
137 64 65 134 136 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) = ( I X ( p ` I ) ) )
138 73 79 oveq12d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ) = ( ( I Y ( p ` I ) ) .+ ( I Z ( p ` I ) ) ) )
139 132 137 138 3eqtr4d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ) )
140 139 oveq1d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r X ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) = ( ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) )
141 102 140 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) = ( ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) )
142 33 94 39 40 50 96 101 gsummptfidmsplit 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Y ( p ` r ) ) ) ) ) )
143 11 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Y |` ( ( N \ { I } ) X. N ) ) )
144 143 oveqd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r ( Y |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) )
145 simpr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> r e. ( N \ { I } ) )
146 83 49 sylan2 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( p ` r ) e. N )
147 ovres 
 |-  ( ( r e. ( N \ { I } ) /\ ( p ` r ) e. N ) -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r X ( p ` r ) ) )
148 145 146 147 syl2anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r ( X |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r X ( p ` r ) ) )
149 ovres 
 |-  ( ( r e. ( N \ { I } ) /\ ( p ` r ) e. N ) -> ( r ( Y |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r Y ( p ` r ) ) )
150 145 146 149 syl2anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r ( Y |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r Y ( p ` r ) ) )
151 144 148 150 3eqtr3rd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r Y ( p ` r ) ) = ( r X ( p ` r ) ) )
152 151 mpteq2dva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( r e. ( N \ { I } ) |-> ( r Y ( p ` r ) ) ) = ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) )
153 152 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Y ( p ` r ) ) ) ) = ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) )
154 153 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Y ( p ` r ) ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) )
155 142 154 eqtrd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) )
156 33 94 39 40 57 96 101 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 ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) )
157 12 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Z |` ( ( N \ { I } ) X. N ) ) )
158 157 oveqd 
 |-  ( ( ( 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 ) ) )
159 ovres 
 |-  ( ( r e. ( N \ { I } ) /\ ( p ` r ) e. N ) -> ( r ( Z |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r Z ( p ` r ) ) )
160 145 146 159 syl2anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r ( Z |` ( ( N \ { I } ) X. N ) ) ( p ` r ) ) = ( r Z ( p ` r ) ) )
161 158 148 160 3eqtr3rd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ r e. ( N \ { I } ) ) -> ( r Z ( p ` r ) ) = ( r X ( p ` r ) ) )
162 161 mpteq2dva 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) = ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) )
163 162 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) = ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) )
164 163 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r Z ( p ` r ) ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) )
165 156 164 eqtrd 
 |-  ( ( 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 ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) )
166 155 165 oveq12d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) = ( ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Y ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) .+ ( ( ( mulGrp ` R ) gsum ( r e. { I } |-> ( r Z ( p ` r ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. ( N \ { I } ) |-> ( r X ( p ` r ) ) ) ) ) ) )
167 93 141 166 3eqtr4rd 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) = ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) )
168 167 oveq2d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) .+ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) )
169 62 168 eqtr3d 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) .+ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) )
170 169 mpteq2dva 
 |-  ( ph -> ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) .+ ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) )
171 21 170 eqtrid 
 |-  ( ph -> ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) oF .+ ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) )
172 171 oveq2d 
 |-  ( ph -> ( R gsum ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) oF .+ ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) ) )
173 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
174 5 22 173 3syl 
 |-  ( ph -> R e. CMnd )
175 46 30 symgbasfi 
 |-  ( N e. Fin -> ( Base ` ( SymGrp ` N ) ) e. Fin )
176 27 175 syl 
 |-  ( ph -> ( Base ` ( SymGrp ` N ) ) e. Fin )
177 32 60 ringcl 
 |-  ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) e. ( Base ` R ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) e. ( Base ` R ) )
178 24 36 52 177 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) e. ( Base ` R ) )
179 32 60 ringcl 
 |-  ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. ( Base ` R ) /\ ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) e. ( Base ` R ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) e. ( Base ` R ) )
180 24 36 59 179 syl3anc 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) e. ( Base ` R ) )
181 32 4 174 176 178 180 15 18 gsummptfidmadd2 
 |-  ( ph -> ( R gsum ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) oF .+ ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) = ( ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) ) .+ ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) )
182 172 181 eqtr3d 
 |-  ( ph -> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) ) = ( ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) ) .+ ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) )
183 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
184 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
185 1 2 3 30 183 184 60 31 mdetleib2 
 |-  ( ( R e. CRing /\ X e. B ) -> ( D ` X ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) ) )
186 5 6 185 syl2anc 
 |-  ( ph -> ( D ` X ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r X ( p ` r ) ) ) ) ) ) ) )
187 1 2 3 30 183 184 60 31 mdetleib2 
 |-  ( ( R e. CRing /\ Y e. B ) -> ( D ` Y ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) ) )
188 5 7 187 syl2anc 
 |-  ( ph -> ( D ` Y ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) ) )
189 1 2 3 30 183 184 60 31 mdetleib2 
 |-  ( ( R e. CRing /\ Z e. B ) -> ( D ` Z ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) )
190 5 8 189 syl2anc 
 |-  ( ph -> ( D ` Z ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) )
191 188 190 oveq12d 
 |-  ( ph -> ( ( D ` Y ) .+ ( D ` Z ) ) = ( ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Y ( p ` r ) ) ) ) ) ) ) .+ ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( r e. N |-> ( r Z ( p ` r ) ) ) ) ) ) ) ) )
192 182 186 191 3eqtr4d 
 |-  ( ph -> ( D ` X ) = ( ( D ` Y ) .+ ( D ` Z ) ) )