Metamath Proof Explorer

Theorem 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 ∈ Fin ∧ R ∈ Ring → S ∈ 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 ∈ Fin ∧ R ∈ Ring → R = Scalar ⁡ A
4 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring → Base R = Base R
5 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring → Base A = Base A
6 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring → + A = + A
7 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring → ⋅ A = ⋅ A
8 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring → LSubSp ⁡ A = LSubSp ⁡ A
9 eqid ⊢ Base R = Base R
10 eqid ⊢ Base A = Base A
11 eqid ⊢ 1 A = 1 A
12 eqid ⊢ ⋅ A = ⋅ A
13 9 1 10 11 12 2 scmatval ⊢ N ∈ Fin ∧ R ∈ Ring → S = m ∈ Base A | ∃ c ∈ Base R m = c ⋅ A 1 A
14 ssrab2 ⊢ m ∈ Base A | ∃ c ∈ Base R m = c ⋅ A 1 A ⊆ Base A
15 13 14 eqsstrdi ⊢ N ∈ Fin ∧ R ∈ Ring → S ⊆ Base A
16 eqid ⊢ 0 R = 0 R
17 1 10 9 16 2 scmatid ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ S
18 17 ne0d ⊢ N ∈ Fin ∧ R ∈ Ring → S ≠ ∅
19 9 1 2 12 smatvscl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ a ∈ Base R ∧ x ∈ S → a ⋅ A x ∈ S
20 19 3adantr3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ a ∈ Base R ∧ x ∈ S ∧ y ∈ S → a ⋅ A x ∈ S
21 simpr3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ a ∈ Base R ∧ x ∈ S ∧ y ∈ S → y ∈ S
22 20 21 jca ⊢ N ∈ Fin ∧ R ∈ Ring ∧ a ∈ Base R ∧ x ∈ S ∧ y ∈ S → a ⋅ A x ∈ S ∧ y ∈ S
23 1 10 9 16 2 scmataddcl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ a ⋅ A x ∈ S ∧ y ∈ S → a ⋅ A x + A y ∈ S
24 22 23 syldan ⊢ N ∈ Fin ∧ R ∈ Ring ∧ a ∈ Base R ∧ x ∈ S ∧ y ∈ S → a ⋅ A x + A y ∈ S
25 3 4 5 6 7 8 15 18 24 islssd ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ LSubSp ⁡ A