scmatsrng

Description: The set of scalar matrices is a subring of the matrix ring/algebra. (Contributed by AV, 21-Aug-2019) (Revised by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatid.a	$⊢ A = N Mat R$
	scmatid.b	$⊢ B = {Base}_{A}$
	scmatid.e	$⊢ E = {Base}_{R}$
	scmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
	scmatid.s	$⊢ S = N ScMat R$
Assertion	scmatsrng	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (A)$

Step	Hyp	Ref	Expression
1		scmatid.a	$⊢ A = N Mat R$
2		scmatid.b	$⊢ B = {Base}_{A}$
3		scmatid.e	$⊢ E = {Base}_{R}$
4		scmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
5		scmatid.s	$⊢ S = N ScMat R$
6	1 2 3 4 5	scmatsgrp	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (A)$
7	1 2 3 4 5	scmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in S$
8	1 2 3 4 5	scmatmulcl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x \cdot_{A} y \in S$
9	8	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \forall y \in S x \cdot_{A} y \in S$
10	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
11		eqid	$⊢ 1_{A} = 1_{A}$
12		eqid	$⊢ \cdot_{A} = \cdot_{A}$
13	2 11 12	issubrg2	$⊢ A \in Ring \to (S \in SubRing (A) \leftrightarrow (S \in SubGrp (A) \land 1_{A} \in S \land \forall x \in S \forall y \in S x \cdot_{A} y \in S))$
14	10 13	syl	$⊢ (N \in Fin \land R \in Ring) \to (S \in SubRing (A) \leftrightarrow (S \in SubGrp (A) \land 1_{A} \in S \land \forall x \in S \forall y \in S x \cdot_{A} y \in S))$
15	6 7 9 14	mpbir3and	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (A)$

Metamath Proof Explorer