Metamath Proof Explorer

Theorem smadiadetlem1

Description: Lemma 1 for smadiadet : A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-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 )
Assertion smadiadetlem1 
|- ( ( ( M e. B /\ K e. N ) /\ p e. P ) -> ( ( ( 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 ) ) ) ) ) e. ( Base ` R ) )

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 1 2 3 4 5 marep01ma 
 |-  ( M e. B -> ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) e. B )
12 11 ad2antrr 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. P ) -> ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) e. B )
13 simpr 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. P ) -> p e. P )
14 6 9 8 1 2 7 madetsmelbas2 
 |-  ( ( R e. CRing /\ ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) e. B /\ p e. P ) -> ( ( ( 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 ) ) ) ) ) e. ( Base ` R ) )
15 3 12 13 14 mp3an2i 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. P ) -> ( ( ( 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 ) ) ) ) ) e. ( Base ` R ) )