Metamath Proof Explorer

Theorem scmatsrng1

Description: The set of scalar matrices is a subring of the ring of diagonal matrices. (Contributed by AV, 21-Aug-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
scmatsgrp1.d ⊢ D = N DMat R
scmatsgrp1.c ⊢ C = A ↾ 𝑠 D
Assertion scmatsrng1 ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ C

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 scmatsgrp1.d ⊢ D = N DMat R
7 scmatsgrp1.c ⊢ C = A ↾ 𝑠 D
8 1 2 3 4 5 6 7 scmatsgrp1 ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubGrp ⁡ C
9 1 2 4 6 dmatsrng ⊢ R ∈ Ring ∧ N ∈ Fin → D ∈ SubRing ⁡ A
10 9 ancoms ⊢ N ∈ Fin ∧ R ∈ Ring → D ∈ SubRing ⁡ A
11 eqid ⊢ 1 A = 1 A
12 7 11 subrg1 ⊢ D ∈ SubRing ⁡ A → 1 A = 1 C
13 10 12 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = 1 C
14 13 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring → 1 C = 1 A
15 1 2 3 4 5 scmatid ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ S
16 14 15 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring → 1 C ∈ S
17 eqid ⊢ ⋅ A = ⋅ A
18 7 17 ressmulr ⊢ D ∈ SubRing ⁡ A → ⋅ A = ⋅ C
19 10 18 syl ⊢ N ∈ Fin ∧ R ∈ Ring → ⋅ A = ⋅ C
20 19 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring → ⋅ C = ⋅ A
21 20 oveqdr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ S ∧ y ∈ S → x ⋅ C y = x ⋅ A y
22 1 2 3 4 5 scmatmulcl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ S ∧ y ∈ S → x ⋅ A y ∈ S
23 21 22 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ S ∧ y ∈ S → x ⋅ C y ∈ S
24 23 ralrimivva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ x ∈ S ∀ y ∈ S x ⋅ C y ∈ S
25 7 subrgring ⊢ D ∈ SubRing ⁡ A → C ∈ Ring
26 eqid ⊢ Base C = Base C
27 eqid ⊢ 1 C = 1 C
28 eqid ⊢ ⋅ C = ⋅ C
29 26 27 28 issubrg2 ⊢ C ∈ Ring → S ∈ SubRing ⁡ C ↔ S ∈ SubGrp ⁡ C ∧ 1 C ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ C y ∈ S
30 10 25 29 3syl ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ C ↔ S ∈ SubGrp ⁡ C ∧ 1 C ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ C y ∈ S
31 8 16 24 30 mpbir3and ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ C