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