dmatsubcl

Description: The difference of two diagonal matrices is a diagonal matrix. (Contributed by AV, 19-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	dmatsubcl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X -_{A} Y \in D$

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	1	matgrp	$⊢ (N \in Fin \land R \in Ring) \to A \in Grp$
6	5	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to A \in Grp$
7	1 2 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (X \in D \to X \in B)$
8	7	imp	$⊢ ((N \in Fin \land R \in Ring) \land X \in D) \to X \in B$
9	8	adantrr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \in B$
10	1 2 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (Y \in D \to Y \in B)$
11	10	imp	$⊢ ((N \in Fin \land R \in Ring) \land Y \in D) \to Y \in B$
12	11	adantrl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to Y \in B$
13		eqid	$⊢ -_{A} = -_{A}$
14	2 13	grpsubcl	$⊢ (A \in Grp \land X \in B \land Y \in B) \to X -_{A} Y \in B$
15	6 9 12 14	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X -_{A} Y \in B$
16		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
17	16	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to R \in Ring$
18	17	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \to R \in Ring$
19	7 10	anim12d	$⊢ (N \in Fin \land R \in Ring) \to ((X \in D \land Y \in D) \to (X \in B \land Y \in B))$
20	19	imp	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (X \in B \land Y \in B)$
21	20	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \to (X \in B \land Y \in B)$
22		simpr	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \to (i \in N \land j \in N)$
23		eqid	$⊢ -_{R} = -_{R}$
24	1 2 13 23	matsubgcell	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (i \in N \land j \in N)) \to i (X -_{A} Y) j = (i X j) -_{R} (i Y j)$
25	18 21 22 24	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \to i (X -_{A} Y) j = (i X j) -_{R} (i Y j)$
26	25	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to i (X -_{A} Y) j = (i X j) -_{R} (i Y j)$
27		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to N \in Fin$
28		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \in D$
29	27 17 28	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (N \in Fin \land R \in Ring \land X \in D)$
30	29	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \to (N \in Fin \land R \in Ring \land X \in D)$
31	30	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to (N \in Fin \land R \in Ring \land X \in D)$
32		simplrl	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to i \in N$
33		simplrr	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to j \in N$
34		simpr	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to i \neq j$
35	1 2 3 4	dmatelnd	$⊢ ((N \in Fin \land R \in Ring \land X \in D) \land (i \in N \land j \in N \land i \neq j)) \to i X j = \underset{˙}{0}$
36	31 32 33 34 35	syl13anc	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to i X j = \underset{˙}{0}$
37		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to Y \in D$
38	27 17 37	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (N \in Fin \land R \in Ring \land Y \in D)$
39	38	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \to (N \in Fin \land R \in Ring \land Y \in D)$
40	39	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to (N \in Fin \land R \in Ring \land Y \in D)$
41	1 2 3 4	dmatelnd	$⊢ ((N \in Fin \land R \in Ring \land Y \in D) \land (i \in N \land j \in N \land i \neq j)) \to i Y j = \underset{˙}{0}$
42	40 32 33 34 41	syl13anc	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to i Y j = \underset{˙}{0}$
43	36 42	oveq12d	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to (i X j) -_{R} (i Y j) = \underset{˙}{0} -_{R} \underset{˙}{0}$
44		ringgrp	$⊢ R \in Ring \to R \in Grp$
45		eqid	$⊢ {Base}_{R} = {Base}_{R}$
46	45 3	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in {Base}_{R}$
47	44 46	jca	$⊢ R \in Ring \to (R \in Grp \land \underset{˙}{0} \in {Base}_{R})$
48	47	adantl	$⊢ (N \in Fin \land R \in Ring) \to (R \in Grp \land \underset{˙}{0} \in {Base}_{R})$
49	45 3 23	grpsubid	$⊢ (R \in Grp \land \underset{˙}{0} \in {Base}_{R}) \to \underset{˙}{0} -_{R} \underset{˙}{0} = \underset{˙}{0}$
50	48 49	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} -_{R} \underset{˙}{0} = \underset{˙}{0}$
51	50	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to \underset{˙}{0} -_{R} \underset{˙}{0} = \underset{˙}{0}$
52	26 43 51	3eqtrd	$⊢ ((((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \land i \neq j) \to i (X -_{A} Y) j = \underset{˙}{0}$
53	52	ex	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land (i \in N \land j \in N)) \to (i \neq j \to i (X -_{A} Y) j = \underset{˙}{0})$
54	53	ralrimivva	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to \forall i \in N \forall j \in N (i \neq j \to i (X -_{A} Y) j = \underset{˙}{0})$
55	1 2 3 4	dmatel	$⊢ (N \in Fin \land R \in Ring) \to (X -_{A} Y \in D \leftrightarrow (X -_{A} Y \in B \land \forall i \in N \forall j \in N (i \neq j \to i (X -_{A} Y) j = \underset{˙}{0})))$
56	55	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (X -_{A} Y \in D \leftrightarrow (X -_{A} Y \in B \land \forall i \in N \forall j \in N (i \neq j \to i (X -_{A} Y) j = \underset{˙}{0})))$
57	15 54 56	mpbir2and	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X -_{A} Y \in D$

Metamath Proof Explorer

Theorem dmatsubcl

Proof