Step |
Hyp |
Ref |
Expression |
1 |
|
marep01ma.a |
|- A = ( N Mat R ) |
2 |
|
marep01ma.b |
|- B = ( Base ` A ) |
3 |
|
marep01ma.r |
|- R e. CRing |
4 |
|
marep01ma.0 |
|- .0. = ( 0g ` R ) |
5 |
|
marep01ma.1 |
|- .1. = ( 1r ` R ) |
6 |
|
smadiadetlem.p |
|- P = ( Base ` ( SymGrp ` N ) ) |
7 |
|
smadiadetlem.g |
|- G = ( mulGrp ` R ) |
8 |
|
madetminlem.y |
|- Y = ( ZRHom ` R ) |
9 |
|
madetminlem.s |
|- S = ( pmSgn ` N ) |
10 |
|
madetminlem.t |
|- .x. = ( .r ` R ) |
11 |
|
smadiadetlem.w |
|- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) ) |
12 |
|
smadiadetlem.z |
|- Z = ( pmSgn ` ( N \ { K } ) ) |
13 |
7
|
crngmgp |
|- ( R e. CRing -> G e. CMnd ) |
14 |
3 13
|
mp1i |
|- ( ( M e. B /\ K e. N ) -> G e. CMnd ) |
15 |
1 2
|
matrcl |
|- ( M e. B -> ( N e. Fin /\ R e. _V ) ) |
16 |
15
|
simpld |
|- ( M e. B -> N e. Fin ) |
17 |
16
|
adantr |
|- ( ( M e. B /\ K e. N ) -> N e. Fin ) |
18 |
14 17
|
jca |
|- ( ( M e. B /\ K e. N ) -> ( G e. CMnd /\ N e. Fin ) ) |
19 |
18
|
adantr |
|- ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> ( G e. CMnd /\ N e. Fin ) ) |
20 |
|
simprl |
|- ( ( ( M e. B /\ K e. N ) /\ ( i e. N /\ j e. N ) ) -> i e. N ) |
21 |
|
simprr |
|- ( ( ( M e. B /\ K e. N ) /\ ( i e. N /\ j e. N ) ) -> j e. N ) |
22 |
2
|
eleq2i |
|- ( M e. B <-> M e. ( Base ` A ) ) |
23 |
22
|
biimpi |
|- ( M e. B -> M e. ( Base ` A ) ) |
24 |
23
|
adantr |
|- ( ( M e. B /\ K e. N ) -> M e. ( Base ` A ) ) |
25 |
24
|
adantr |
|- ( ( ( M e. B /\ K e. N ) /\ ( i e. N /\ j e. N ) ) -> M e. ( Base ` A ) ) |
26 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
27 |
1 26
|
matecl |
|- ( ( i e. N /\ j e. N /\ M e. ( Base ` A ) ) -> ( i M j ) e. ( Base ` R ) ) |
28 |
20 21 25 27
|
syl3anc |
|- ( ( ( M e. B /\ K e. N ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. ( Base ` R ) ) |
29 |
7 26
|
mgpbas |
|- ( Base ` R ) = ( Base ` G ) |
30 |
28 29
|
eleqtrdi |
|- ( ( ( M e. B /\ K e. N ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. ( Base ` G ) ) |
31 |
30
|
ralrimivva |
|- ( ( M e. B /\ K e. N ) -> A. i e. N A. j e. N ( i M j ) e. ( Base ` G ) ) |
32 |
31
|
adantr |
|- ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> A. i e. N A. j e. N ( i M j ) e. ( Base ` G ) ) |
33 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
34 |
26 4
|
ring0cl |
|- ( R e. Ring -> .0. e. ( Base ` R ) ) |
35 |
3 33 34
|
mp2b |
|- .0. e. ( Base ` R ) |
36 |
35 29
|
eleqtri |
|- .0. e. ( Base ` G ) |
37 |
32 36
|
jctir |
|- ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> ( A. i e. N A. j e. N ( i M j ) e. ( Base ` G ) /\ .0. e. ( Base ` G ) ) ) |
38 |
|
simpr |
|- ( ( M e. B /\ K e. N ) -> K e. N ) |
39 |
38
|
adantr |
|- ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> K e. N ) |
40 |
|
simpr |
|- ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> p e. { q e. P | ( q ` K ) = K } ) |
41 |
|
eqid |
|- { q e. P | ( q ` K ) = K } = { q e. P | ( q ` K ) = K } |
42 |
7 5
|
ringidval |
|- .1. = ( 0g ` G ) |
43 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
44 |
6 41 42 43
|
gsummatr01 |
|- ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i M j ) e. ( Base ` G ) /\ .0. e. ( Base ` G ) ) /\ ( K e. N /\ K e. N /\ p e. { q e. P | ( q ` K ) = K } ) ) -> ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) |
45 |
19 37 39 39 40 44
|
syl113anc |
|- ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) |
46 |
45
|
oveq2d |
|- ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) = ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) |
47 |
46
|
mpteq2dva |
|- ( ( M e. B /\ K e. N ) -> ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) = ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) |
48 |
47
|
oveq2d |
|- ( ( M e. B /\ K e. N ) -> ( R gsum ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsum ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) ) |
49 |
1 2 3 4 5 6 7 8 9 10 11 12
|
smadiadetlem3 |
|- ( ( M e. B /\ K e. N ) -> ( R gsum ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsum ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) ) |
50 |
48 49
|
eqtrd |
|- ( ( M e. B /\ K e. N ) -> ( R gsum ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsum ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) ) |