Metamath Proof Explorer

Theorem madetsmelbas2

Description: A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019)

Ref Expression
Hypotheses madetsmelbas.p 
|- P = ( Base ` ( SymGrp ` N ) )
madetsmelbas.s 
|- S = ( pmSgn ` N )
madetsmelbas.y 
|- Y = ( ZRHom ` R )
madetsmelbas.a 
|- A = ( N Mat R )
madetsmelbas.b 
|- B = ( Base ` A )
madetsmelbas.g 
|- G = ( mulGrp ` R )
Assertion madetsmelbas2 
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> ( ( ( Y o. S ) ` Q ) ( .r ` R ) ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) ) e. ( Base ` R ) )

Proof

Step Hyp Ref Expression
1 madetsmelbas.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 madetsmelbas.s 
 |-  S = ( pmSgn ` N )
3 madetsmelbas.y 
 |-  Y = ( ZRHom ` R )
4 madetsmelbas.a 
 |-  A = ( N Mat R )
5 madetsmelbas.b 
 |-  B = ( Base ` A )
6 madetsmelbas.g 
 |-  G = ( mulGrp ` R )
7 crngring 
 |-  ( R e. CRing -> R e. Ring )
8 7 3ad2ant1 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> R e. Ring )
9 4 5 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
10 9 simpld 
 |-  ( M e. B -> N e. Fin )
11 10 3ad2ant2 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> N e. Fin )
12 simp3 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> Q e. P )
13 1 2 3 zrhcopsgnelbas 
 |-  ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) e. ( Base ` R ) )
14 8 11 12 13 syl3anc 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> ( ( Y o. S ) ` Q ) e. ( Base ` R ) )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 6 15 mgpbas 
 |-  ( Base ` R ) = ( Base ` G )
17 6 crngmgp 
 |-  ( R e. CRing -> G e. CMnd )
18 17 3ad2ant1 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> G e. CMnd )
19 simp2 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> M e. B )
20 4 5 1 matepm2cl 
 |-  ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( n M ( Q ` n ) ) e. ( Base ` R ) )
21 8 12 19 20 syl3anc 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> A. n e. N ( n M ( Q ` n ) ) e. ( Base ` R ) )
22 16 18 11 21 gsummptcl 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) e. ( Base ` R ) )
23 eqid 
 |-  ( .r ` R ) = ( .r ` R )
24 15 23 ringcl 
 |-  ( ( R e. Ring /\ ( ( Y o. S ) ` Q ) e. ( Base ` R ) /\ ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) e. ( Base ` R ) ) -> ( ( ( Y o. S ) ` Q ) ( .r ` R ) ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) ) e. ( Base ` R ) )
25 8 14 22 24 syl3anc 
 |-  ( ( R e. CRing /\ M e. B /\ Q e. P ) -> ( ( ( Y o. S ) ` Q ) ( .r ` R ) ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) ) e. ( Base ` R ) )