dmatsgrp

Description: The set of diagonal matrices is a subgroup of the matrix group/algebra. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	dmatid.a	$⊢ A = N Mat R$
	dmatid.b	$⊢ B = {Base}_{A}$
	dmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
	dmatid.d	$⊢ D = N DMat R$
Assertion	dmatsgrp	$⊢ (R \in Ring \land N \in Fin) \to D \in SubGrp (A)$

Proof

Step	Hyp	Ref	Expression
1		dmatid.a	$⊢ A = N Mat R$
2		dmatid.b	$⊢ B = {Base}_{A}$
3		dmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
4		dmatid.d	$⊢ D = N DMat R$
5	1 2 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (z \in D \to z \in B)$
6	5	ancoms	$⊢ (R \in Ring \land N \in Fin) \to (z \in D \to z \in B)$
7	6	ssrdv	$⊢ (R \in Ring \land N \in Fin) \to D \subseteq B$
8	1 2 3 4	dmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in D$
9	8	ancoms	$⊢ (R \in Ring \land N \in Fin) \to 1_{A} \in D$
10	9	ne0d	$⊢ (R \in Ring \land N \in Fin) \to D \neq \emptyset$
11	1 2 3 4	dmatsubcl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in D \land y \in D)) \to x -_{A} y \in D$
12	11	ancom1s	$⊢ ((R \in Ring \land N \in Fin) \land (x \in D \land y \in D)) \to x -_{A} y \in D$
13	12	ralrimivva	$⊢ (R \in Ring \land N \in Fin) \to \forall x \in D \forall y \in D x -_{A} y \in D$
14	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
15	14	ancoms	$⊢ (R \in Ring \land N \in Fin) \to A \in Ring$
16		ringgrp	$⊢ A \in Ring \to A \in Grp$
17		eqid	$⊢ -_{A} = -_{A}$
18	2 17	issubg4	$⊢ A \in Grp \to (D \in SubGrp (A) \leftrightarrow (D \subseteq B \land D \neq \emptyset \land \forall x \in D \forall y \in D x -_{A} y \in D))$
19	15 16 18	3syl	$⊢ (R \in Ring \land N \in Fin) \to (D \in SubGrp (A) \leftrightarrow (D \subseteq B \land D \neq \emptyset \land \forall x \in D \forall y \in D x -_{A} y \in D))$
20	7 10 13 19	mpbir3and	$⊢ (R \in Ring \land N \in Fin) \to D \in SubGrp (A)$

Metamath Proof Explorer

Theorem dmatsgrp

Proof