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	syl5eq	$⊢ ((((((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	biimpi	$⊢ c \in K \to c \in {Base}_{R}$
73	72	adantl	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to c \in {Base}_{R}$
74	73	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}$
75		eqid	$⊢ {Base}_{R} = {Base}_{R}$
76	2 75 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}$
77	75 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}$
78	50 74 76 77	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}$
79	78	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}$
80	31 64 66 38 70 79	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))$
81	48 61 80	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))$
82		csbov2g	$⊢ i \in N \to ⦋ i / k ⦌ (c \cdot_{R} (k m j)) = c \cdot_{R} ⦋ i / k ⦌ (k m j)$
83		csbov1g	$⊢ i \in N \to ⦋ i / k ⦌ (k m j) = ⦋ i / k ⦌ k m j$
84		csbvarg	$⊢ i \in N \to ⦋ i / k ⦌ k = i$
85	84	oveq1d	$⊢ i \in N \to ⦋ i / k ⦌ k m j = i m j$
86	83 85	eqtrd	$⊢ i \in N \to ⦋ i / k ⦌ (k m j) = i m j$
87	86	oveq2d	$⊢ i \in N \to c \cdot_{R} ⦋ i / k ⦌ (k m j) = c \cdot_{R} (i m j)$
88	82 87	eqtrd	$⊢ i \in N \to ⦋ i / k ⦌ (c \cdot_{R} (k m j)) = c \cdot_{R} (i m j)$
89	88	adantr	$⊢ (i \in N \land j \in N) \to ⦋ i / k ⦌ (c \cdot_{R} (k m j)) = c \cdot_{R} (i m j)$
90	89	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)$
91	26 81 90	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)$
92		simpr	$⊢ (((N \in Fin \land R \in Ring) \land C \in S) \land c \in K) \to c \in K$
93	92	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)$
94	93	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)$
95	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)$
96	12 94 24 95	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)$
97	91 96	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$
98	97	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$
99	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$
100	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$
101	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$
102	99 100 52 101	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$
103	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)$
104	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$
105	103 93 104	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$
106	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)$
107	102 105 106	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)$
108	98 107	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$
109	10 108	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$
110	109	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)$
111	110	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)$
112	111	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)$
113	9 112	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