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 \in CRing \land M \in B \land Q \in P) \to (Y \circ S) (Q) \cdot_{R} (\underset{n \in N}{\sum_{G}}, (n M Q (n))) \in {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 \in CRing \to R \in Ring$
8	7	3ad2ant1	$⊢ (R \in CRing \land M \in B \land Q \in P) \to R \in Ring$
9	4 5	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
10	9	simpld	$⊢ M \in B \to N \in Fin$
11	10	3ad2ant2	$⊢ (R \in CRing \land M \in B \land Q \in P) \to N \in Fin$
12		simp3	$⊢ (R \in CRing \land M \in B \land Q \in P) \to Q \in P$
13	1 2 3	zrhcopsgnelbas	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to (Y \circ S) (Q) \in {Base}_{R}$
14	8 11 12 13	syl3anc	$⊢ (R \in CRing \land M \in B \land Q \in P) \to (Y \circ S) (Q) \in {Base}_{R}$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	6 15	mgpbas	$⊢ {Base}_{R} = {Base}_{G}$
17	6	crngmgp	$⊢ R \in CRing \to G \in CMnd$
18	17	3ad2ant1	$⊢ (R \in CRing \land M \in B \land Q \in P) \to G \in CMnd$
19		simp2	$⊢ (R \in CRing \land M \in B \land Q \in P) \to M \in B$
20	4 5 1	matepm2cl	$⊢ (R \in Ring \land Q \in P \land M \in B) \to \forall n \in N n M Q (n) \in {Base}_{R}$
21	8 12 19 20	syl3anc	$⊢ (R \in CRing \land M \in B \land Q \in P) \to \forall n \in N n M Q (n) \in {Base}_{R}$
22	16 18 11 21	gsummptcl	$⊢ (R \in CRing \land M \in B \land Q \in P) \to \underset{n \in N}{\sum_{G}} (n M Q (n)) \in {Base}_{R}$
23		eqid	$⊢ \cdot_{R} = \cdot_{R}$
24	15 23	ringcl	$⊢ (R \in Ring \land (Y \circ S) (Q) \in {Base}_{R} \land \underset{n \in N}{\sum_{G}} (n M Q (n)) \in {Base}_{R}) \to (Y \circ S) (Q) \cdot_{R} (\underset{n \in N}{\sum_{G}}, (n M Q (n))) \in {Base}_{R}$
25	8 14 22 24	syl3anc	$⊢ (R \in CRing \land M \in B \land Q \in P) \to (Y \circ S) (Q) \cdot_{R} (\underset{n \in N}{\sum_{G}}, (n M Q (n))) \in {Base}_{R}$

Metamath Proof Explorer

Theorem madetsmelbas2

Proof