scmatcrng

Description: The subring of scalar matrices (over a commutative ring) is a commutative ring. (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$
	scmatcrng.c	$⊢ C = A ↾_{𝑠} S$
Assertion	scmatcrng	$⊢ (N \in Fin \land R \in CRing) \to C \in CRing$

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		scmatcrng.c	$⊢ C = A ↾_{𝑠} S$
7		crngring	$⊢ R \in CRing \to R \in Ring$
8	1 2 3 4 5	scmatsrng	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (A)$
9	7 8	sylan2	$⊢ (N \in Fin \land R \in CRing) \to S \in SubRing (A)$
10	6	subrgring	$⊢ S \in SubRing (A) \to C \in Ring$
11	9 10	syl	$⊢ (N \in Fin \land R \in CRing) \to C \in Ring$
12		simp1lr	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to R \in CRing$
13		eqid	$⊢ {Base}_{A} = {Base}_{A}$
14		simp2	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to a \in N$
15		simp3	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to b \in N$
16	1 13 5	scmatmat	$⊢ (N \in Fin \land R \in CRing) \to (x \in S \to x \in {Base}_{A})$
17	16	imp	$⊢ ((N \in Fin \land R \in CRing) \land x \in S) \to x \in {Base}_{A}$
18	17	adantrr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \to x \in {Base}_{A}$
19	18	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to x \in {Base}_{A}$
20	1 3 13 14 15 19	matecld	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to a x b \in E$
21	1 13 5	scmatmat	$⊢ (N \in Fin \land R \in CRing) \to (y \in S \to y \in {Base}_{A})$
22	21	imp	$⊢ ((N \in Fin \land R \in CRing) \land y \in S) \to y \in {Base}_{A}$
23	22	adantrl	$⊢ ((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \to y \in {Base}_{A}$
24	23	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to y \in {Base}_{A}$
25	1 3 13 14 15 24	matecld	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to a y b \in E$
26		eqid	$⊢ \cdot_{R} = \cdot_{R}$
27	3 26	crngcom	$⊢ (R \in CRing \land a x b \in E \land a y b \in E) \to (a x b) \cdot_{R} (a y b) = (a y b) \cdot_{R} (a x b)$
28	12 20 25 27	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to (a x b) \cdot_{R} (a y b) = (a y b) \cdot_{R} (a x b)$
29	28	ifeq1d	$⊢ (((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \land a \in N \land b \in N) \to if (a = b, (a x b) \cdot_{R} (a y b), \underset{˙}{0}) = if (a = b, (a y b) \cdot_{R} (a x b), \underset{˙}{0})$
30	29	mpoeq3dva	$⊢ ((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \to (a \in N, b \in N ⟼ if (a = b, (a x b) \cdot_{R} (a y b), \underset{˙}{0})) = (a \in N, b \in N ⟼ if (a = b, (a y b) \cdot_{R} (a x b), \underset{˙}{0}))$
31	7	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
32		eqid	$⊢ N DMat R = N DMat R$
33	1 2 3 4 5 32	scmatdmat	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to x \in (N DMat R))$
34	7 33	sylan2	$⊢ (N \in Fin \land R \in CRing) \to (x \in S \to x \in (N DMat R))$
35	1 2 3 4 5 32	scmatdmat	$⊢ (N \in Fin \land R \in Ring) \to (y \in S \to y \in (N DMat R))$
36	7 35	sylan2	$⊢ (N \in Fin \land R \in CRing) \to (y \in S \to y \in (N DMat R))$
37	34 36	anim12d	$⊢ (N \in Fin \land R \in CRing) \to ((x \in S \land y \in S) \to (x \in (N DMat R) \land y \in (N DMat R)))$
38	37	imp	$⊢ ((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \to (x \in (N DMat R) \land y \in (N DMat R))$
39	1 2 4 32	dmatmul	$⊢ ((N \in Fin \land R \in Ring) \land (x \in (N DMat R) \land y \in (N DMat R))) \to x \cdot_{A} y = (a \in N, b \in N ⟼ if (a = b, (a x b) \cdot_{R} (a y b), \underset{˙}{0}))$
40	31 38 39	syl2an2r	$⊢ ((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \to x \cdot_{A} y = (a \in N, b \in N ⟼ if (a = b, (a x b) \cdot_{R} (a y b), \underset{˙}{0}))$
41	38	ancomd	$⊢ ((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \to (y \in (N DMat R) \land x \in (N DMat R))$
42	1 2 4 32	dmatmul	$⊢ ((N \in Fin \land R \in Ring) \land (y \in (N DMat R) \land x \in (N DMat R))) \to y \cdot_{A} x = (a \in N, b \in N ⟼ if (a = b, (a y b) \cdot_{R} (a x b), \underset{˙}{0}))$
43	31 41 42	syl2an2r	$⊢ ((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \to y \cdot_{A} x = (a \in N, b \in N ⟼ if (a = b, (a y b) \cdot_{R} (a x b), \underset{˙}{0}))$
44	30 40 43	3eqtr4d	$⊢ ((N \in Fin \land R \in CRing) \land (x \in S \land y \in S)) \to x \cdot_{A} y = y \cdot_{A} x$
45	44	ralrimivva	$⊢ (N \in Fin \land R \in CRing) \to \forall x \in S \forall y \in S x \cdot_{A} y = y \cdot_{A} x$
46	6	subrgbas	$⊢ S \in SubRing (A) \to S = {Base}_{C}$
47	46	eqcomd	$⊢ S \in SubRing (A) \to {Base}_{C} = S$
48		eqid	$⊢ \cdot_{A} = \cdot_{A}$
49	6 48	ressmulr	$⊢ S \in SubRing (A) \to \cdot_{A} = \cdot_{C}$
50	49	eqcomd	$⊢ S \in SubRing (A) \to \cdot_{C} = \cdot_{A}$
51	50	oveqd	$⊢ S \in SubRing (A) \to x \cdot_{C} y = x \cdot_{A} y$
52	50	oveqd	$⊢ S \in SubRing (A) \to y \cdot_{C} x = y \cdot_{A} x$
53	51 52	eqeq12d	$⊢ S \in SubRing (A) \to (x \cdot_{C} y = y \cdot_{C} x \leftrightarrow x \cdot_{A} y = y \cdot_{A} x)$
54	47 53	raleqbidv	$⊢ S \in SubRing (A) \to (\forall y \in {Base}_{C} x \cdot_{C} y = y \cdot_{C} x \leftrightarrow \forall y \in S x \cdot_{A} y = y \cdot_{A} x)$
55	47 54	raleqbidv	$⊢ S \in SubRing (A) \to (\forall x \in {Base}_{C} \forall y \in {Base}_{C} x \cdot_{C} y = y \cdot_{C} x \leftrightarrow \forall x \in S \forall y \in S x \cdot_{A} y = y \cdot_{A} x)$
56	9 55	syl	$⊢ (N \in Fin \land R \in CRing) \to (\forall x \in {Base}_{C} \forall y \in {Base}_{C} x \cdot_{C} y = y \cdot_{C} x \leftrightarrow \forall x \in S \forall y \in S x \cdot_{A} y = y \cdot_{A} x)$
57	45 56	mpbird	$⊢ (N \in Fin \land R \in CRing) \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} x \cdot_{C} y = y \cdot_{C} x$
58		eqid	$⊢ {Base}_{C} = {Base}_{C}$
59		eqid	$⊢ \cdot_{C} = \cdot_{C}$
60	58 59	iscrng2	$⊢ C \in CRing \leftrightarrow (C \in Ring \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} x \cdot_{C} y = y \cdot_{C} x)$
61	11 57 60	sylanbrc	$⊢ (N \in Fin \land R \in CRing) \to C \in CRing$

Metamath Proof Explorer

Theorem scmatcrng

Proof