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 = ℤRHom R
madetsmelbas.a A = N Mat R
madetsmelbas.b B = Base A
madetsmelbas.g G = mulGrp R
Assertion madetsmelbas2 R CRing M B Q P Y S Q R G n N n M Q n Base R

Proof

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