dmatscmcl

Description: The multiplication of a diagonal matrix with a scalar is a diagonal matrix. (Contributed by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	dmatscmcl.k	$⊢ K = {Base}_{R}$
	dmatscmcl.a	$⊢ A = N Mat R$
	dmatscmcl.b	$⊢ B = {Base}_{A}$
	dmatscmcl.s	$⊢ \underset{˙}{*} = \cdot_{A}$
	dmatscmcl.d	$⊢ D = N DMat R$
Assertion	dmatscmcl	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in D)) \to C \underset{˙}{*} M \in D$

Proof

Step	Hyp	Ref	Expression
1		dmatscmcl.k	$⊢ K = {Base}_{R}$
2		dmatscmcl.a	$⊢ A = N Mat R$
3		dmatscmcl.b	$⊢ B = {Base}_{A}$
4		dmatscmcl.s	$⊢ \underset{˙}{*} = \cdot_{A}$
5		dmatscmcl.d	$⊢ D = N DMat R$
6		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in D)) \to C \in K$
7		eqid	$⊢ 0_{R} = 0_{R}$
8	2 3 7 5	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (M \in D \to M \in B)$
9	8	com12	$⊢ M \in D \to ((N \in Fin \land R \in Ring) \to M \in B)$
10	9	adantl	$⊢ (C \in K \land M \in D) \to ((N \in Fin \land R \in Ring) \to M \in B)$
11	10	impcom	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in D)) \to M \in B$
12	6 11	jca	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in D)) \to (C \in K \land M \in B)$
13	1 2 3 4	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in B)) \to C \underset{˙}{*} M \in B$
14	12 13	syldan	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in D)) \to C \underset{˙}{*} M \in B$
15	2 3 7 5	dmatel	$⊢ (N \in Fin \land R \in Ring) \to (M \in D \leftrightarrow (M \in B \land \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R})))$
16	15	adantr	$⊢ ((N \in Fin \land R \in Ring) \land C \in K) \to (M \in D \leftrightarrow (M \in B \land \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R})))$
17		simp-4r	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \to R \in Ring$
18		simpr	$⊢ ((N \in Fin \land R \in Ring) \land C \in K) \to C \in K$
19	18	anim1i	$⊢ (((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \to (C \in K \land M \in B)$
20	19	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \to (C \in K \land M \in B)$
21		simpr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \to (i \in N \land j \in N)$
22	17 20 21	3jca	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \to (R \in Ring \land (C \in K \land M \in B) \land (i \in N \land j \in N))$
23	22	adantr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \land i M j = 0_{R}) \to (R \in Ring \land (C \in K \land M \in B) \land (i \in N \land j \in N))$
24		eqid	$⊢ \cdot_{R} = \cdot_{R}$
25	2 3 1 4 24	matvscacell	$⊢ (R \in Ring \land (C \in K \land M \in B) \land (i \in N \land j \in N)) \to i (C \underset{˙}{*} M) j = C \cdot_{R} (i M j)$
26	23 25	syl	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \land i M j = 0_{R}) \to i (C \underset{˙}{*} M) j = C \cdot_{R} (i M j)$
27		oveq2	$⊢ i M j = 0_{R} \to C \cdot_{R} (i M j) = C \cdot_{R} 0_{R}$
28	27	adantl	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \land i M j = 0_{R}) \to C \cdot_{R} (i M j) = C \cdot_{R} 0_{R}$
29	1 24 7	ringrz	$⊢ (R \in Ring \land C \in K) \to C \cdot_{R} 0_{R} = 0_{R}$
30	29	ad5ant23	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \to C \cdot_{R} 0_{R} = 0_{R}$
31	30	adantr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \land i M j = 0_{R}) \to C \cdot_{R} 0_{R} = 0_{R}$
32	26 28 31	3eqtrd	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \land i M j = 0_{R}) \to i (C \underset{˙}{*} M) j = 0_{R}$
33	32	ex	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \to (i M j = 0_{R} \to i (C \underset{˙}{*} M) j = 0_{R})$
34	33	imim2d	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \land (i \in N \land j \in N)) \to ((i \neq j \to i M j = 0_{R}) \to (i \neq j \to i (C \underset{˙}{*} M) j = 0_{R}))$
35	34	ralimdvva	$⊢ (((N \in Fin \land R \in Ring) \land C \in K) \land M \in B) \to (\forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R}) \to \forall i \in N \forall j \in N (i \neq j \to i (C \underset{˙}{*} M) j = 0_{R}))$
36	35	expimpd	$⊢ ((N \in Fin \land R \in Ring) \land C \in K) \to ((M \in B \land \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R})) \to \forall i \in N \forall j \in N (i \neq j \to i (C \underset{˙}{*} M) j = 0_{R}))$
37	16 36	sylbid	$⊢ ((N \in Fin \land R \in Ring) \land C \in K) \to (M \in D \to \forall i \in N \forall j \in N (i \neq j \to i (C \underset{˙}{*} M) j = 0_{R}))$
38	37	impr	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in D)) \to \forall i \in N \forall j \in N (i \neq j \to i (C \underset{˙}{*} M) j = 0_{R})$
39	2 3 7 5	dmatel	$⊢ (N \in Fin \land R \in Ring) \to (C \underset{˙}{} M \in D \leftrightarrow (C \underset{˙}{} M \in B \land \forall i \in N \forall j \in N (i \neq j \to i (C \underset{˙}{*} M) j = 0_{R})))$
40	39	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in D)) \to (C \underset{˙}{} M \in D \leftrightarrow (C \underset{˙}{} M \in B \land \forall i \in N \forall j \in N (i \neq j \to i (C \underset{˙}{*} M) j = 0_{R})))$
41	14 38 40	mpbir2and	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land M \in D)) \to C \underset{˙}{*} M \in D$

Metamath Proof Explorer

Theorem dmatscmcl

Proof