dmatmulcl

Description: The product of two diagonal matrices is a diagonal matrix. (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$
Assertion	dmatmulcl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \cdot_{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		oveq	$⊢ m = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) \to i m j = i (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) j$
6	5	eqeq1d	$⊢ m = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) \to (i m j = \underset{˙}{0} \leftrightarrow i (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) j = \underset{˙}{0})$
7	6	imbi2d	$⊢ m = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) \to ((i \neq j \to i m j = \underset{˙}{0}) \leftrightarrow (i \neq j \to i (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) j = \underset{˙}{0}))$
8	7	2ralbidv	$⊢ m = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) \to (\forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0}) \leftrightarrow \forall i \in N \forall j \in N (i \neq j \to i (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) j = \underset{˙}{0}))$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to N \in Fin$
11		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to R \in Ring$
12	11	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to R \in Ring$
13		eqid	$⊢ {Base}_{A} = {Base}_{A}$
14		simp2	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to x \in N$
15		simp3	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to y \in N$
16	1 13 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (X \in D \to X \in {Base}_{A})$
17	16	imp	$⊢ ((N \in Fin \land R \in Ring) \land X \in D) \to X \in {Base}_{A}$
18	17	adantrr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \in {Base}_{A}$
19	18	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to X \in {Base}_{A}$
20	1 9 13 14 15 19	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to x X y \in {Base}_{R}$
21	1 13 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (Y \in D \to Y \in {Base}_{A})$
22	21	imp	$⊢ ((N \in Fin \land R \in Ring) \land Y \in D) \to Y \in {Base}_{A}$
23	22	adantrl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to Y \in {Base}_{A}$
24	23	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to Y \in {Base}_{A}$
25	1 9 13 14 15 24	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to x Y y \in {Base}_{R}$
26		eqid	$⊢ \cdot_{R} = \cdot_{R}$
27	9 26	ringcl	$⊢ (R \in Ring \land x X y \in {Base}_{R} \land x Y y \in {Base}_{R}) \to (x X y) \cdot_{R} (x Y y) \in {Base}_{R}$
28	12 20 25 27	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to (x X y) \cdot_{R} (x Y y) \in {Base}_{R}$
29	9 3	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in {Base}_{R}$
30	29	adantl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} \in {Base}_{R}$
31	30	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to \underset{˙}{0} \in {Base}_{R}$
32	31	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to \underset{˙}{0} \in {Base}_{R}$
33	28 32	ifcld	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}) \in {Base}_{R}$
34	1 9 2 10 11 33	matbas2d	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) \in B$
35		eqidd	$⊢ ((((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 (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}))$
36		eqeq12	$⊢ (x = i \land y = j) \to (x = y \leftrightarrow i = j)$
37		oveq12	$⊢ (x = i \land y = j) \to x X y = i X j$
38		oveq12	$⊢ (x = i \land y = j) \to x Y y = i Y j$
39	37 38	oveq12d	$⊢ (x = i \land y = j) \to (x X y) \cdot_{R} (x Y y) = (i X j) \cdot_{R} (i Y j)$
40	36 39	ifbieq1d	$⊢ (x = i \land y = j) \to if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}) = if (i = j, (i X j) \cdot_{R} (i Y j), \underset{˙}{0})$
41	40	adantl	$⊢ (((((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) \land (x = i \land y = j)) \to if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}) = if (i = j, (i X j) \cdot_{R} (i Y j), \underset{˙}{0})$
42		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$
43		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$
44		ovex	$⊢ (i X j) \cdot_{R} (i Y j) \in V$
45	3	fvexi	$⊢ \underset{˙}{0} \in V$
46	44 45	ifex	$⊢ if (i = j, (i X j) \cdot_{R} (i Y j), \underset{˙}{0}) \in V$
47	46	a1i	$⊢ ((((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 if (i = j, (i X j) \cdot_{R} (i Y j), \underset{˙}{0}) \in V$
48	35 41 42 43 47	ovmpod	$⊢ ((((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 \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) j = if (i = j, (i X j) \cdot_{R} (i Y j), \underset{˙}{0})$
49		ifnefalse	$⊢ i \neq j \to if (i = j, (i X j) \cdot_{R} (i Y j), \underset{˙}{0}) = \underset{˙}{0}$
50	49	adantl	$⊢ ((((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 if (i = j, (i X j) \cdot_{R} (i Y j), \underset{˙}{0}) = \underset{˙}{0}$
51	48 50	eqtrd	$⊢ ((((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 \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) j = \underset{˙}{0}$
52	51	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 \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) j = \underset{˙}{0})$
53	52	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 \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) j = \underset{˙}{0})$
54	8 34 53	elrabd	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})) \in \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\}$
55	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 = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}))$
56	1 2 3 4	dmatval	$⊢ (N \in Fin \land R \in Ring) \to D = \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\}$
57	56	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to D = \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\}$
58	54 55 57	3eltr4d	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \cdot_{A} Y \in D$

Metamath Proof Explorer

Theorem dmatmulcl

Proof