scmatscm

Description: The multiplication of a matrix with a scalar matrix corresponds to a scalar multiplication. (Contributed by AV, 28-Dec-2019)

	Ref	Expression
Hypotheses	scmatscm.k	$⊢ K = {Base}_{R}$
	scmatscm.a	$⊢ A = N Mat R$
	scmatscm.b	$⊢ B = {Base}_{A}$
	scmatscm.t	$⊢ \underset{˙}{*} = \cdot_{A}$
	scmatscm.m	$⊢ \underset{˙}{\times} = \cdot_{A}$
	scmatscm.c	$⊢ S = N ScMat R$
Assertion	scmatscm	$⊢ ((N \in Fin \land R \in Ring) \land C \in S) \to \exists c \in K \forall m \in B C \underset{˙}{\times} m = c \underset{˙}{*} m$

Proof

Step	Hyp	Ref	Expression
1		scmatscm.k	$⊢ K = {Base}_{R}$
2		scmatscm.a	$⊢ A = N Mat R$
3		scmatscm.b	$⊢ B = {Base}_{A}$
4		scmatscm.t	$⊢ \underset{˙}{*} = \cdot_{A}$
5		scmatscm.m	$⊢ \underset{˙}{\times} = \cdot_{A}$
6		scmatscm.c	$⊢ S = N ScMat R$
7		eqid	$⊢ 1_{A} = 1_{A}$
8	1 2 3 7 4 6	scmatscmid	$⊢ (N \in Fin \land R \in Ring \land C \in S) \to \exists c \in K C = c \underset{˙}{*} 1_{A}$
9	8	3expa	$⊢ ((N \in Fin \land R \in Ring) \land C \in S) \to \exists c \in K C = c \underset{˙}{*} 1_{A}$
10		oveq1	$⊢ C = c \underset{˙}{} 1_{A} \to C \underset{˙}{\times} m = (c \underset{˙}{} 1_{A}) \underset{˙}{\times} m$
11		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
12	11	ad4antr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to R \in Ring$
13		simpl	$⊢ ((N \in Fin \land R \in Ring) \land C \in S) \to (N \in Fin \land R \in Ring)$
14	13	adantr	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to (N \in Fin \land R \in Ring)$
15	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
16	3 7	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
17	15 16	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in B$
18	17	adantr	$⊢ ((N \in Fin \land R \in Ring) \land C \in S) \to 1_{A} \in B$
19	18	anim1ci	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to (c \in K \land 1_{A} \in B)$
20	1 2 3 4	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (c \in K \land 1_{A} \in B)) \to c \underset{˙}{*} 1_{A} \in B$
21	14 19 20	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to c \underset{˙}{*} 1_{A} \in B$
22	21	anim1i	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to (c \underset{˙}{*} 1_{A} \in B \land m \in B)$
23	22	adantr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to (c \underset{˙}{*} 1_{A} \in B \land m \in B)$
24		simpr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to (i \in N \land j \in N)$
25	2 3 5	matmulcell	$⊢ (R \in Ring \land (c \underset{˙}{} 1_{A} \in B \land m \in B) \land (i \in N \land j \in N)) \to i ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m) j = \underset{k \in N}{\sum_{R}} ((i (c \underset{˙}{*} 1_{A}) k) \cdot_{R} (k m j))$
26	12 23 24 25	syl3anc	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to i ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m) j = \underset{k \in N}{\sum_{R}} ((i (c \underset{˙}{} 1_{A}) k) \cdot_{R} (k m j))$
27	13	anim1i	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to ((N \in Fin \land R \in Ring) \land c \in K)$
28		df-3an	$⊢ (N \in Fin \land R \in Ring \land c \in K) \leftrightarrow ((N \in Fin \land R \in Ring) \land c \in K)$
29	27 28	sylibr	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to (N \in Fin \land R \in Ring \land c \in K)$
30	29	ad3antrrr	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to (N \in Fin \land R \in Ring \land c \in K)$
31		eqid	$⊢ 0_{R} = 0_{R}$
32	2 1 4 31	matsc	$⊢ (N \in Fin \land R \in Ring \land c \in K) \to c \underset{˙}{*} 1_{A} = (x \in N, y \in N ⟼ if (x = y, c, 0_{R}))$
33	30 32	syl	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to c \underset{˙}{*} 1_{A} = (x \in N, y \in N ⟼ if (x = y, c, 0_{R}))$
34		eqeq12	$⊢ (x = i \land y = k) \to (x = y \leftrightarrow i = k)$
35	34	ifbid	$⊢ (x = i \land y = k) \to if (x = y, c, 0_{R}) = if (i = k, c, 0_{R})$
36	35	adantl	$⊢ (((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \land (x = i \land y = k)) \to if (x = y, c, 0_{R}) = if (i = k, c, 0_{R})$
37		simpl	$⊢ (i \in N \land j \in N) \to i \in N$
38	37	adantl	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to i \in N$
39	38	adantr	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to i \in N$
40		simpr	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to k \in N$
41		vex	$⊢ c \in V$
42		fvex	$⊢ 0_{R} \in V$
43	41 42	ifex	$⊢ if (i = k, c, 0_{R}) \in V$
44	43	a1i	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to if (i = k, c, 0_{R}) \in V$
45	33 36 39 40 44	ovmpod	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to i (c \underset{˙}{*} 1_{A}) k = if (i = k, c, 0_{R})$
46	45	oveq1d	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to (i (c \underset{˙}{*} 1_{A}) k) \cdot_{R} (k m j) = if (i = k, c, 0_{R}) \cdot_{R} (k m j)$
47	46	mpteq2dva	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to (k \in N ⟼ (i (c \underset{˙}{*} 1_{A}) k) \cdot_{R} (k m j)) = (k \in N ⟼ if (i = k, c, 0_{R}) \cdot_{R} (k m j))$
48	47	oveq2d	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to \underset{k \in N}{\sum_{R}} ((i (c \underset{˙}{*} 1_{A}) k) \cdot_{R} (k m j)) = \underset{k \in N}{\sum_{R}} (if (i = k, c, 0_{R}) \cdot_{R} (k m j))$
49		ovif	$⊢ if (i = k, c, 0_{R}) \cdot_{R} (k m j) = if (i = k, c \cdot_{R} (k m j), 0_{R} \cdot_{R} (k m j))$
50		simp-6r	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to R \in Ring$
51		simplrr	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to j \in N$
52		simpr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to m \in B$
53	52	ad2antrr	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to m \in B$
54	2 1 3 40 51 53	matecld	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to k m j \in K$
55		eqid	$⊢ \cdot_{R} = \cdot_{R}$
56	1 55 31	ringlz	$⊢ (R \in Ring \land k m j \in K) \to 0_{R} \cdot_{R} (k m j) = 0_{R}$
57	50 54 56	syl2anc	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to 0_{R} \cdot_{R} (k m j) = 0_{R}$
58	57	ifeq2d	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to if (i = k, c \cdot_{R} (k m j), 0_{R} \cdot_{R} (k m j)) = if (i = k, c \cdot_{R} (k m j), 0_{R})$
59	49 58	eqtrid	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to if (i = k, c, 0_{R}) \cdot_{R} (k m j) = if (i = k, c \cdot_{R} (k m j), 0_{R})$
60	59	mpteq2dva	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to (k \in N ⟼ if (i = k, c, 0_{R}) \cdot_{R} (k m j)) = (k \in N ⟼ if (i = k, c \cdot_{R} (k m j), 0_{R}))$
61	60	oveq2d	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to \underset{k \in N}{\sum_{R}} (if (i = k, c, 0_{R}) \cdot_{R} (k m j)) = \underset{k \in N}{\sum_{R}} if (i = k, c \cdot_{R} (k m j), 0_{R})$
62		ringmnd	$⊢ R \in Ring \to R \in Mnd$
63	62	adantl	$⊢ (N \in Fin \land R \in Ring) \to R \in Mnd$
64	63	ad4antr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to R \in Mnd$
65		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
66	65	ad4antr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to N \in Fin$
67		equcom	$⊢ i = k \leftrightarrow k = i$
68		ifbi	$⊢ (i = k \leftrightarrow k = i) \to if (i = k, c \cdot_{R} (k m j), 0_{R}) = if (k = i, c \cdot_{R} (k m j), 0_{R})$
69	67 68	ax-mp	$⊢ if (i = k, c \cdot_{R} (k m j), 0_{R}) = if (k = i, c \cdot_{R} (k m j), 0_{R})$
70	69	mpteq2i	$⊢ (k \in N ⟼ if (i = k, c \cdot_{R} (k m j), 0_{R})) = (k \in N ⟼ if (k = i, c \cdot_{R} (k m j), 0_{R}))$
71	1	eleq2i	$⊢ c \in K \leftrightarrow c \in {Base}_{R}$
72	71	bilani	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to c \in {Base}_{R}$
73	72	ad3antrrr	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to c \in {Base}_{R}$
74		eqid	$⊢ {Base}_{R} = {Base}_{R}$
75	2 74 3 40 51 53	matecld	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to k m j \in {Base}_{R}$
76	74 55	ringcl	$⊢ (R \in Ring \land c \in {Base}_{R} \land k m j \in {Base}_{R}) \to c \cdot_{R} (k m j) \in {Base}_{R}$
77	50 73 75 76	syl3anc	$⊢ ((((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \land k \in N) \to c \cdot_{R} (k m j) \in {Base}_{R}$
78	77	ralrimiva	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to \forall k \in N c \cdot_{R} (k m j) \in {Base}_{R}$
79	31 64 66 38 70 78	gsummpt1n0	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to \underset{k \in N}{\sum_{R}} if (i = k, c \cdot_{R} (k m j), 0_{R}) = ⦋ i / k ⦌ (c \cdot_{R} (k m j))$
80	48 61 79	3eqtrd	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to \underset{k \in N}{\sum_{R}} ((i (c \underset{˙}{*} 1_{A}) k) \cdot_{R} (k m j)) = ⦋ i / k ⦌ (c \cdot_{R} (k m j))$
81		csbov2g	$⊢ i \in N \to ⦋ i / k ⦌ (c \cdot_{R} (k m j)) = c \cdot_{R} ⦋ i / k ⦌ (k m j)$
82		csbov1g	$⊢ i \in N \to ⦋ i / k ⦌ (k m j) = ⦋ i / k ⦌ k m j$
83		csbvarg	$⊢ i \in N \to ⦋ i / k ⦌ k = i$
84	83	oveq1d	$⊢ i \in N \to ⦋ i / k ⦌ k m j = i m j$
85	82 84	eqtrd	$⊢ i \in N \to ⦋ i / k ⦌ (k m j) = i m j$
86	85	oveq2d	$⊢ i \in N \to c \cdot_{R} ⦋ i / k ⦌ (k m j) = c \cdot_{R} (i m j)$
87	81 86	eqtrd	$⊢ i \in N \to ⦋ i / k ⦌ (c \cdot_{R} (k m j)) = c \cdot_{R} (i m j)$
88	87	adantr	$⊢ (i \in N \land j \in N) \to ⦋ i / k ⦌ (c \cdot_{R} (k m j)) = c \cdot_{R} (i m j)$
89	88	adantl	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to ⦋ i / k ⦌ (c \cdot_{R} (k m j)) = c \cdot_{R} (i m j)$
90	26 80 89	3eqtrd	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to i ((c \underset{˙}{*} 1_{A}) \underset{˙}{\times} m) j = c \cdot_{R} (i m j)$
91		simpr	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to c \in K$
92	91	anim1i	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to (c \in K \land m \in B)$
93	92	adantr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to (c \in K \land m \in B)$
94	2 3 1 4 55	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)$
95	12 93 24 94	syl3anc	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \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)$
96	90 95	eqtr4d	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land (i \in N \land j \in N)) \to i ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m) j = i (c \underset{˙}{} m) j$
97	96	ralrimivva	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to \forall i \in N \forall j \in N i ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m) j = i (c \underset{˙}{} m) j$
98	15	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to A \in Ring$
99	21	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to c \underset{˙}{*} 1_{A} \in B$
100	3 5	ringcl	$⊢ (A \in Ring \land c \underset{˙}{} 1_{A} \in B \land m \in B) \to (c \underset{˙}{} 1_{A}) \underset{˙}{\times} m \in B$
101	98 99 52 100	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to (c \underset{˙}{*} 1_{A}) \underset{˙}{\times} m \in B$
102	13	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to (N \in Fin \land R \in Ring)$
103	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$
104	102 92 103	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to c \underset{˙}{*} m \in B$
105	2 3	eqmat	$⊢ ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m \in B \land c \underset{˙}{} m \in B) \to ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m = c \underset{˙}{} m \leftrightarrow \forall i \in N \forall j \in N i ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m) j = i (c \underset{˙}{} m) j)$
106	101 104 105	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m = c \underset{˙}{} m \leftrightarrow \forall i \in N \forall j \in N i ((c \underset{˙}{} 1_{A}) \underset{˙}{\times} m) j = i (c \underset{˙}{} m) j)$
107	97 106	mpbird	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to (c \underset{˙}{} 1_{A}) \underset{˙}{\times} m = c \underset{˙}{} m$
108	10 107	sylan9eqr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \land C = c \underset{˙}{} 1_{A}) \to C \underset{˙}{\times} m = c \underset{˙}{} m$
109	108	ex	$⊢ ((((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \land m \in B) \to (C = c \underset{˙}{} 1_{A} \to C \underset{˙}{\times} m = c \underset{˙}{} m)$
110	109	ralrimdva	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to (C = c \underset{˙}{} 1_{A} \to \forall m \in B C \underset{˙}{\times} m = c \underset{˙}{} m)$
111	110	reximdva	$⊢ ((N \in Fin \land R \in Ring) \land C \in S) \to (\exists c \in K C = c \underset{˙}{} 1_{A} \to \exists c \in K \forall m \in B C \underset{˙}{\times} m = c \underset{˙}{} m)$
112	9 111	mpd	$⊢ ((N \in Fin \land R \in Ring) \land C \in S) \to \exists c \in K \forall m \in B C \underset{˙}{\times} m = c \underset{˙}{*} m$

Metamath Proof Explorer

Theorem scmatscm

Proof