dmatsrng

Description: The set of diagonal matrices is a subring of the matrix ring/algebra. (Contributed by AV, 20-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	dmatsrng	$⊢ (R \in Ring \land N \in Fin) \to D \in SubRing (A)$

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	dmatsgrp	$⊢ (R \in Ring \land N \in Fin) \to D \in SubGrp (A)$
6	1 2 3 4	dmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in D$
7	6	ancoms	$⊢ (R \in Ring \land N \in Fin) \to 1_{A} \in D$
8	1 2 3 4	dmatmulcl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in D \land y \in D)) \to x \cdot_{A} y \in D$
9	8	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in D \forall y \in D x \cdot_{A} y \in D$
10	9	ancoms	$⊢ (R \in Ring \land N \in Fin) \to \forall x \in D \forall y \in D x \cdot_{A} y \in D$
11	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
12	11	ancoms	$⊢ (R \in Ring \land N \in Fin) \to A \in Ring$
13		eqid	$⊢ 1_{A} = 1_{A}$
14		eqid	$⊢ \cdot_{A} = \cdot_{A}$
15	2 13 14	issubrg2	$⊢ A \in Ring \to (D \in SubRing (A) \leftrightarrow (D \in SubGrp (A) \land 1_{A} \in D \land \forall x \in D \forall y \in D x \cdot_{A} y \in D))$
16	12 15	syl	$⊢ (R \in Ring \land N \in Fin) \to (D \in SubRing (A) \leftrightarrow (D \in SubGrp (A) \land 1_{A} \in D \land \forall x \in D \forall y \in D x \cdot_{A} y \in D))$
17	5 7 10 16	mpbir3and	$⊢ (R \in Ring \land N \in Fin) \to D \in SubRing (A)$

Metamath Proof Explorer