scmatmulcl

Description: The product of two scalar matrices is a scalar matrix. (Contributed by AV, 21-Aug-2019) (Revised by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatid.a	$⊢ A = N Mat R$
	scmatid.b	$⊢ B = {Base}_{A}$
	scmatid.e	$⊢ E = {Base}_{R}$
	scmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
	scmatid.s	$⊢ S = N ScMat R$
Assertion	scmatmulcl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in S \land Y \in S)) \to X \cdot_{A} Y \in S$

Proof

Step	Hyp	Ref	Expression
1		scmatid.a	$⊢ A = N Mat R$
2		scmatid.b	$⊢ B = {Base}_{A}$
3		scmatid.e	$⊢ E = {Base}_{R}$
4		scmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
5		scmatid.s	$⊢ S = N ScMat R$
6		eqid	$⊢ 1_{A} = 1_{A}$
7		eqid	$⊢ \cdot_{A} = \cdot_{A}$
8	3 1 2 6 7 5	scmatel	$⊢ (N \in Fin \land R \in Ring) \to (X \in S \leftrightarrow (X \in B \land \exists c \in E X = c \cdot_{A} 1_{A}))$
9	3 1 2 6 7 5	scmatel	$⊢ (N \in Fin \land R \in Ring) \to (Y \in S \leftrightarrow (Y \in B \land \exists d \in E Y = d \cdot_{A} 1_{A}))$
10		oveq12	$⊢ (X = c \cdot_{A} 1_{A} \land Y = d \cdot_{A} 1_{A}) \to X \cdot_{A} Y = (c \cdot_{A} 1_{A}) \cdot_{A} (d \cdot_{A} 1_{A})$
11	10	adantll	$⊢ (((((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \land X = c \cdot_{A} 1_{A}) \land Y = d \cdot_{A} 1_{A}) \to X \cdot_{A} Y = (c \cdot_{A} 1_{A}) \cdot_{A} (d \cdot_{A} 1_{A})$
12		simp-4l	$⊢ (((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \to (N \in Fin \land R \in Ring)$
13		simplr	$⊢ ((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \to d \in E$
14	13	anim1ci	$⊢ (((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \to (c \in E \land d \in E)$
15		eqid	$⊢ \cdot_{R} = \cdot_{R}$
16		eqid	$⊢ \cdot_{A} = \cdot_{A}$
17	1 3 4 6 7 15 16	scmatscmiddistr	$⊢ ((N \in Fin \land R \in Ring) \land (c \in E \land d \in E)) \to (c \cdot_{A} 1_{A}) \cdot_{A} (d \cdot_{A} 1_{A}) = (c \cdot_{R} d) \cdot_{A} 1_{A}$
18	12 14 17	syl2anc	$⊢ (((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \to (c \cdot_{A} 1_{A}) \cdot_{A} (d \cdot_{A} 1_{A}) = (c \cdot_{R} d) \cdot_{A} 1_{A}$
19		simpl	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to (N \in Fin \land R \in Ring)$
20		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to R \in Ring$
21		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to c \in E$
22		simpl	$⊢ (d \in E \land c \in E) \to d \in E$
23	22	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to d \in E$
24	3 15	ringcl	$⊢ (R \in Ring \land c \in E \land d \in E) \to c \cdot_{R} d \in E$
25	20 21 23 24	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to c \cdot_{R} d \in E$
26	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
27	2 6	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
28	26 27	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in B$
29	28	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to 1_{A} \in B$
30	3 1 2 7	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (c \cdot_{R} d \in E \land 1_{A} \in B)) \to (c \cdot_{R} d) \cdot_{A} 1_{A} \in B$
31	19 25 29 30	syl12anc	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to (c \cdot_{R} d) \cdot_{A} 1_{A} \in B$
32		oveq1	$⊢ e = c \cdot_{R} d \to e \cdot_{A} 1_{A} = (c \cdot_{R} d) \cdot_{A} 1_{A}$
33	32	eqeq2d	$⊢ e = c \cdot_{R} d \to ((c \cdot_{R} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A} \leftrightarrow (c \cdot_{R} d) \cdot_{A} 1_{A} = (c \cdot_{R} d) \cdot_{A} 1_{A})$
34	33	adantl	$⊢ (((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \land e = c \cdot_{R} d) \to ((c \cdot_{R} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A} \leftrightarrow (c \cdot_{R} d) \cdot_{A} 1_{A} = (c \cdot_{R} d) \cdot_{A} 1_{A})$
35		eqidd	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to (c \cdot_{R} d) \cdot_{A} 1_{A} = (c \cdot_{R} d) \cdot_{A} 1_{A}$
36	25 34 35	rspcedvd	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to \exists e \in E (c \cdot_{R} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A}$
37	3 1 2 6 7 5	scmatel	$⊢ (N \in Fin \land R \in Ring) \to ((c \cdot_{R} d) \cdot_{A} 1_{A} \in S \leftrightarrow ((c \cdot_{R} d) \cdot_{A} 1_{A} \in B \land \exists e \in E (c \cdot_{R} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A}))$
38	37	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to ((c \cdot_{R} d) \cdot_{A} 1_{A} \in S \leftrightarrow ((c \cdot_{R} d) \cdot_{A} 1_{A} \in B \land \exists e \in E (c \cdot_{R} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A}))$
39	31 36 38	mpbir2and	$⊢ ((N \in Fin \land R \in Ring) \land (d \in E \land c \in E)) \to (c \cdot_{R} d) \cdot_{A} 1_{A} \in S$
40	39	exp32	$⊢ (N \in Fin \land R \in Ring) \to (d \in E \to (c \in E \to (c \cdot_{R} d) \cdot_{A} 1_{A} \in S))$
41	40	adantr	$⊢ ((N \in Fin \land R \in Ring) \land Y \in B) \to (d \in E \to (c \in E \to (c \cdot_{R} d) \cdot_{A} 1_{A} \in S))$
42	41	imp	$⊢ (((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \to (c \in E \to (c \cdot_{R} d) \cdot_{A} 1_{A} \in S)$
43	42	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \to (c \in E \to (c \cdot_{R} d) \cdot_{A} 1_{A} \in S)$
44	43	imp	$⊢ (((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \to (c \cdot_{R} d) \cdot_{A} 1_{A} \in S$
45	18 44	eqeltrd	$⊢ (((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \to (c \cdot_{A} 1_{A}) \cdot_{A} (d \cdot_{A} 1_{A}) \in S$
46	45	adantr	$⊢ ((((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \land X = c \cdot_{A} 1_{A}) \to (c \cdot_{A} 1_{A}) \cdot_{A} (d \cdot_{A} 1_{A}) \in S$
47	46	adantr	$⊢ (((((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \land X = c \cdot_{A} 1_{A}) \land Y = d \cdot_{A} 1_{A}) \to (c \cdot_{A} 1_{A}) \cdot_{A} (d \cdot_{A} 1_{A}) \in S$
48	11 47	eqeltrd	$⊢ (((((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \land X = c \cdot_{A} 1_{A}) \land Y = d \cdot_{A} 1_{A}) \to X \cdot_{A} Y \in S$
49	48	exp31	$⊢ (((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \land c \in E) \to (X = c \cdot_{A} 1_{A} \to (Y = d \cdot_{A} 1_{A} \to X \cdot_{A} Y \in S))$
50	49	rexlimdva	$⊢ ((((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \land X \in B) \to (\exists c \in E X = c \cdot_{A} 1_{A} \to (Y = d \cdot_{A} 1_{A} \to X \cdot_{A} Y \in S))$
51	50	expimpd	$⊢ (((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \to ((X \in B \land \exists c \in E X = c \cdot_{A} 1_{A}) \to (Y = d \cdot_{A} 1_{A} \to X \cdot_{A} Y \in S))$
52	51	com23	$⊢ (((N \in Fin \land R \in Ring) \land Y \in B) \land d \in E) \to (Y = d \cdot_{A} 1_{A} \to ((X \in B \land \exists c \in E X = c \cdot_{A} 1_{A}) \to X \cdot_{A} Y \in S))$
53	52	rexlimdva	$⊢ ((N \in Fin \land R \in Ring) \land Y \in B) \to (\exists d \in E Y = d \cdot_{A} 1_{A} \to ((X \in B \land \exists c \in E X = c \cdot_{A} 1_{A}) \to X \cdot_{A} Y \in S))$
54	53	expimpd	$⊢ (N \in Fin \land R \in Ring) \to ((Y \in B \land \exists d \in E Y = d \cdot_{A} 1_{A}) \to ((X \in B \land \exists c \in E X = c \cdot_{A} 1_{A}) \to X \cdot_{A} Y \in S))$
55	9 54	sylbid	$⊢ (N \in Fin \land R \in Ring) \to (Y \in S \to ((X \in B \land \exists c \in E X = c \cdot_{A} 1_{A}) \to X \cdot_{A} Y \in S))$
56	55	com23	$⊢ (N \in Fin \land R \in Ring) \to ((X \in B \land \exists c \in E X = c \cdot_{A} 1_{A}) \to (Y \in S \to X \cdot_{A} Y \in S))$
57	8 56	sylbid	$⊢ (N \in Fin \land R \in Ring) \to (X \in S \to (Y \in S \to X \cdot_{A} Y \in S))$
58	57	imp32	$⊢ ((N \in Fin \land R \in Ring) \land (X \in S \land Y \in S)) \to X \cdot_{A} Y \in S$

Metamath Proof Explorer

Theorem scmatmulcl

Proof