Metamath Proof Explorer

Theorem scmatsrng

Description: The set of scalar matrices is a subring of the matrix ring/algebra. (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 ⊢ 0 ˙ = 0 R
scmatid.s ⊢ S = N ScMat R
Assertion scmatsrng ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ A

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 ⊢ 0 ˙ = 0 R
5 scmatid.s ⊢ S = N ScMat R
6 1 2 3 4 5 scmatsgrp ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubGrp ⁡ A
7 1 2 3 4 5 scmatid ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ S
8 1 2 3 4 5 scmatmulcl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ S ∧ y ∈ S → x ⋅ A y ∈ S
9 8 ralrimivva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ x ∈ S ∀ y ∈ S x ⋅ A y ∈ S
10 1 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
11 eqid ⊢ 1 A = 1 A
12 eqid ⊢ ⋅ A = ⋅ A
13 2 11 12 issubrg2 ⊢ A ∈ Ring → S ∈ SubRing ⁡ A ↔ S ∈ SubGrp ⁡ A ∧ 1 A ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ A y ∈ S
14 10 13 syl ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ A ↔ S ∈ SubGrp ⁡ A ∧ 1 A ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ A y ∈ S
15 6 7 9 14 mpbir3and ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ A