scmatsgrp1

Description: The set of scalar matrices is a subgroup of the group/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	scmatsgrp1	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (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	scmatdmat	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to x \in D)$
9	8	ssrdv	$⊢ (N \in Fin \land R \in Ring) \to S \subseteq D$
10	1 2 4 6	dmatsgrp	$⊢ (R \in Ring \land N \in Fin) \to D \in SubGrp (A)$
11	10	ancoms	$⊢ (N \in Fin \land R \in Ring) \to D \in SubGrp (A)$
12	7	subgbas	$⊢ D \in SubGrp (A) \to D = {Base}_{C}$
13	12	eqcomd	$⊢ D \in SubGrp (A) \to {Base}_{C} = D$
14	11 13	syl	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{C} = D$
15	9 14	sseqtrrd	$⊢ (N \in Fin \land R \in Ring) \to S \subseteq {Base}_{C}$
16	1 2 3 4 5	scmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in S$
17	16	ne0d	$⊢ (N \in Fin \land R \in Ring) \to S \neq \emptyset$
18	11	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to D \in SubGrp (A)$
19	8	com12	$⊢ x \in S \to ((N \in Fin \land R \in Ring) \to x \in D)$
20	19	adantr	$⊢ (x \in S \land y \in S) \to ((N \in Fin \land R \in Ring) \to x \in D)$
21	20	impcom	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x \in D$
22	1 2 3 4 5 6	scmatdmat	$⊢ (N \in Fin \land R \in Ring) \to (y \in S \to y \in D)$
23	22	a1d	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to (y \in S \to y \in D))$
24	23	imp32	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to y \in D$
25		eqid	$⊢ -_{A} = -_{A}$
26		eqid	$⊢ -_{C} = -_{C}$
27	25 7 26	subgsub	$⊢ (D \in SubGrp (A) \land x \in D \land y \in D) \to x -_{A} y = x -_{C} y$
28	27	eqcomd	$⊢ (D \in SubGrp (A) \land x \in D \land y \in D) \to x -_{C} y = x -_{A} y$
29	18 21 24 28	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x -_{C} y = x -_{A} y$
30	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$
31	29 30	eqeltrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x -_{C} y \in S$
32	31	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \forall y \in S x -_{C} y \in S$
33	1 2 4 6	dmatsrng	$⊢ (R \in Ring \land N \in Fin) \to D \in SubRing (A)$
34	33	ancoms	$⊢ (N \in Fin \land R \in Ring) \to D \in SubRing (A)$
35	7	subrgring	$⊢ D \in SubRing (A) \to C \in Ring$
36		ringgrp	$⊢ C \in Ring \to C \in Grp$
37		eqid	$⊢ {Base}_{C} = {Base}_{C}$
38	37 26	issubg4	$⊢ C \in Grp \to (S \in SubGrp (C) \leftrightarrow (S \subseteq {Base}_{C} \land S \neq \emptyset \land \forall x \in S \forall y \in S x -_{C} y \in S))$
39	34 35 36 38	4syl	$⊢ (N \in Fin \land R \in Ring) \to (S \in SubGrp (C) \leftrightarrow (S \subseteq {Base}_{C} \land S \neq \emptyset \land \forall x \in S \forall y \in S x -_{C} y \in S))$
40	15 17 32 39	mpbir3and	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (C)$

Metamath Proof Explorer

Theorem scmatsgrp1

Proof