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 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 ) ) ) ) ) ) ) )