scmatsrng1

Description: The set of scalar matrices is a subring of the ring of diagonal matrices. (Contributed by AV, 21-Aug-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$
	scmatsgrp1.d	$⊢ D = N DMat R$
	scmatsgrp1.c	$⊢ C = A ↾_{𝑠} D$
Assertion	scmatsrng1	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (C)$

Proof

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		scmatsgrp1.d	$⊢ D = N DMat R$
7		scmatsgrp1.c	$⊢ C = A ↾_{𝑠} D$
8	1 2 3 4 5 6 7	scmatsgrp1	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (C)$
9	1 2 4 6	dmatsrng	$⊢ (R \in Ring \land N \in Fin) \to D \in SubRing (A)$
10	9	ancoms	$⊢ (N \in Fin \land R \in Ring) \to D \in SubRing (A)$
11		eqid	$⊢ 1_{A} = 1_{A}$
12	7 11	subrg1	$⊢ D \in SubRing (A) \to 1_{A} = 1_{C}$
13	10 12	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} = 1_{C}$
14	13	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to 1_{C} = 1_{A}$
15	1 2 3 4 5	scmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in S$
16	14 15	eqeltrd	$⊢ (N \in Fin \land R \in Ring) \to 1_{C} \in S$
17		eqid	$⊢ \cdot_{A} = \cdot_{A}$
18	7 17	ressmulr	$⊢ D \in SubRing (A) \to \cdot_{A} = \cdot_{C}$
19	10 18	syl	$⊢ (N \in Fin \land R \in Ring) \to \cdot_{A} = \cdot_{C}$
20	19	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to \cdot_{C} = \cdot_{A}$
21	20	oveqdr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x \cdot_{C} y = x \cdot_{A} y$
22	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$
23	21 22	eqeltrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x \cdot_{C} y \in S$
24	23	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \forall y \in S x \cdot_{C} y \in S$
25	7	subrgring	$⊢ D \in SubRing (A) \to C \in Ring$
26		eqid	$⊢ {Base}_{C} = {Base}_{C}$
27		eqid	$⊢ 1_{C} = 1_{C}$
28		eqid	$⊢ \cdot_{C} = \cdot_{C}$
29	26 27 28	issubrg2	$⊢ C \in Ring \to (S \in SubRing (C) \leftrightarrow (S \in SubGrp (C) \land 1_{C} \in S \land \forall x \in S \forall y \in S x \cdot_{C} y \in S))$
30	10 25 29	3syl	$⊢ (N \in Fin \land R \in Ring) \to (S \in SubRing (C) \leftrightarrow (S \in SubGrp (C) \land 1_{C} \in S \land \forall x \in S \forall y \in S x \cdot_{C} y \in S))$
31	8 16 24 30	mpbir3and	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (C)$

Metamath Proof Explorer

Theorem scmatsrng1

Proof