scmatlss

Description: The set of scalar matrices is a linear subspace of the matrix algebra. (Contributed by AV, 25-Dec-2019)

	Ref	Expression
Hypotheses	scmatlss.a	$⊢ A = N Mat R$
	scmatlss.s	$⊢ S = N ScMat R$
Assertion	scmatlss	$⊢ (N \in Fin \land R \in Ring) \to S \in LSubSp (A)$

Proof

Step	Hyp	Ref	Expression
1		scmatlss.a	$⊢ A = N Mat R$
2		scmatlss.s	$⊢ S = N ScMat R$
3	1	matsca2	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (A)$
4		eqidd	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R} = {Base}_{R}$
5		eqidd	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{A} = {Base}_{A}$
6		eqidd	$⊢ (N \in Fin \land R \in Ring) \to +_{A} = +_{A}$
7		eqidd	$⊢ (N \in Fin \land R \in Ring) \to \cdot_{A} = \cdot_{A}$
8		eqidd	$⊢ (N \in Fin \land R \in Ring) \to LSubSp (A) = LSubSp (A)$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		eqid	$⊢ {Base}_{A} = {Base}_{A}$
11		eqid	$⊢ 1_{A} = 1_{A}$
12		eqid	$⊢ \cdot_{A} = \cdot_{A}$
13	9 1 10 11 12 2	scmatval	$⊢ (N \in Fin \land R \in Ring) \to S = \{m \in {Base}_{A} \| \exists c \in {Base}_{R} m = c \cdot_{A} 1_{A}\}$
14		ssrab2	$⊢ \{m \in {Base}_{A} \| \exists c \in {Base}_{R} m = c \cdot_{A} 1_{A}\} \subseteq {Base}_{A}$
15	13 14	eqsstrdi	$⊢ (N \in Fin \land R \in Ring) \to S \subseteq {Base}_{A}$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	1 10 9 16 2	scmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in S$
18	17	ne0d	$⊢ (N \in Fin \land R \in Ring) \to S \neq \emptyset$
19	9 1 2 12	smatvscl	$⊢ ((N \in Fin \land R \in Ring) \land (a \in {Base}_{R} \land x \in S)) \to a \cdot_{A} x \in S$
20	19	3adantr3	$⊢ ((N \in Fin \land R \in Ring) \land (a \in {Base}_{R} \land x \in S \land y \in S)) \to a \cdot_{A} x \in S$
21		simpr3	$⊢ ((N \in Fin \land R \in Ring) \land (a \in {Base}_{R} \land x \in S \land y \in S)) \to y \in S$
22	20 21	jca	$⊢ ((N \in Fin \land R \in Ring) \land (a \in {Base}_{R} \land x \in S \land y \in S)) \to (a \cdot_{A} x \in S \land y \in S)$
23	1 10 9 16 2	scmataddcl	$⊢ ((N \in Fin \land R \in Ring) \land (a \cdot_{A} x \in S \land y \in S)) \to (a \cdot_{A} x) +_{A} y \in S$
24	22 23	syldan	$⊢ ((N \in Fin \land R \in Ring) \land (a \in {Base}_{R} \land x \in S \land y \in S)) \to (a \cdot_{A} x) +_{A} y \in S$
25	3 4 5 6 7 8 15 18 24	islssd	$⊢ (N \in Fin \land R \in Ring) \to S \in LSubSp (A)$

Metamath Proof Explorer

Theorem scmatlss

Proof