scmatsgrp

Description: The set of scalar matrices is a subgroup of the matrix group/algebra. (Contributed by AV, 20-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	scmatsgrp	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (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 5	scmatmat	$⊢ (N \in Fin \land R \in Ring) \to (z \in S \to z \in B)$
7	6	ssrdv	$⊢ (N \in Fin \land R \in Ring) \to S \subseteq B$
8	1 2 3 4 5	scmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in S$
9	8	ne0d	$⊢ (N \in Fin \land R \in Ring) \to S \neq \emptyset$
10	1 2 3 4 5	scmatsubcl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x -_{A} y \in S$
11	10	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \forall y \in S x -_{A} y \in S$
12	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
13		ringgrp	$⊢ A \in Ring \to A \in Grp$
14		eqid	$⊢ -_{A} = -_{A}$
15	2 14	issubg4	$⊢ A \in Grp \to (S \in SubGrp (A) \leftrightarrow (S \subseteq B \land S \neq \emptyset \land \forall x \in S \forall y \in S x -_{A} y \in S))$
16	12 13 15	3syl	$⊢ (N \in Fin \land R \in Ring) \to (S \in SubGrp (A) \leftrightarrow (S \subseteq B \land S \neq \emptyset \land \forall x \in S \forall y \in S x -_{A} y \in S))$
17	7 9 11 16	mpbir3and	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (A)$

Metamath Proof Explorer