dmatcrng

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

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

Metamath Proof Explorer

Theorem dmatcrng

Proof