Metamath Proof Explorer

Theorem smadiadetlem4

Description: Lemma 4 for smadiadet . (Contributed by AV, 31-Jan-2019)

Ref Expression
Hypotheses marep01ma.a 
|- A = ( N Mat R )
marep01ma.b 
|- B = ( Base ` A )
marep01ma.r 
|- R e. CRing
marep01ma.0 
|- .0. = ( 0g ` R )
marep01ma.1 
|- .1. = ( 1r ` R )
smadiadetlem.p 
|- P = ( Base ` ( SymGrp ` N ) )
smadiadetlem.g 
|- G = ( mulGrp ` R )
madetminlem.y 
|- Y = ( ZRHom ` R )
madetminlem.s 
|- S = ( pmSgn ` N )
madetminlem.t 
|- .x. = ( .r ` R )
smadiadetlem.w 
|- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
smadiadetlem.z 
|- Z = ( pmSgn ` ( N \ { K } ) )
Assertion smadiadetlem4 
|- ( ( 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 ) ) ) ) ) ) ) )

Proof

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 birani 
 |-  ( ( M e. B /\ K e. N ) -> M e. ( Base ` A ) )
24 23 adantr 
 |-  ( ( ( M e. B /\ K e. N ) /\ ( i e. N /\ j e. N ) ) -> M e. ( Base ` A ) )
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 1 25 matecl 
 |-  ( ( i e. N /\ j e. N /\ M e. ( Base ` A ) ) -> ( i M j ) e. ( Base ` R ) )
27 20 21 24 26 syl3anc 
 |-  ( ( ( M e. B /\ K e. N ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. ( Base ` R ) )
28 7 25 mgpbas 
 |-  ( Base ` R ) = ( Base ` G )
29 27 28 eleqtrdi 
 |-  ( ( ( M e. B /\ K e. N ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. ( Base ` G ) )
30 29 ralrimivva 
 |-  ( ( M e. B /\ K e. N ) -> A. i e. N A. j e. N ( i M j ) e. ( Base ` G ) )
31 30 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 ) )
32 crngring 
 |-  ( R e. CRing -> R e. Ring )
33 25 4 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
34 3 32 33 mp2b 
 |-  .0. e. ( Base ` R )
35 34 28 eleqtri 
 |-  .0. e. ( Base ` G )
36 31 35 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 ) ) )
37 simpr 
 |-  ( ( M e. B /\ K e. N ) -> K e. N )
38 37 adantr 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> K e. N )
39 simpr 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> p e. { q e. P | ( q ` K ) = K } )
40 eqid 
 |-  { q e. P | ( q ` K ) = K } = { q e. P | ( q ` K ) = K }
41 7 5 ringidval 
 |-  .1. = ( 0g ` G )
42 eqid 
 |-  ( Base ` G ) = ( Base ` G )
43 6 40 41 42 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 ) ) ) ) )
44 19 36 38 38 39 43 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 ) ) ) ) )
45 44 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 ) ) ) ) ) )
46 45 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 ) ) ) ) ) ) )
47 46 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 ) ) ) ) ) ) ) )
48 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 ) ) ) ) ) ) ) )
49 47 48 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 ) ) ) ) ) ) ) )