Metamath Proof Explorer


Theorem dmatsrng

Description: The set of diagonal matrices is a subring of the matrix ring/algebra. (Contributed by AV, 20-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatid.a 𝐴 = ( 𝑁 Mat 𝑅 )
dmatid.b 𝐵 = ( Base ‘ 𝐴 )
dmatid.0 0 = ( 0g𝑅 )
dmatid.d 𝐷 = ( 𝑁 DMat 𝑅 )
Assertion dmatsrng ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dmatid.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 dmatid.b 𝐵 = ( Base ‘ 𝐴 )
3 dmatid.0 0 = ( 0g𝑅 )
4 dmatid.d 𝐷 = ( 𝑁 DMat 𝑅 )
5 1 2 3 4 dmatsgrp ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubGrp ‘ 𝐴 ) )
6 1 2 3 4 dmatid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r𝐴 ) ∈ 𝐷 )
7 6 ancoms ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 1r𝐴 ) ∈ 𝐷 )
8 1 2 3 4 dmatmulcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) → ( 𝑥 ( .r𝐴 ) 𝑦 ) ∈ 𝐷 )
9 8 ralrimivva ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥𝐷𝑦𝐷 ( 𝑥 ( .r𝐴 ) 𝑦 ) ∈ 𝐷 )
10 9 ancoms ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ∀ 𝑥𝐷𝑦𝐷 ( 𝑥 ( .r𝐴 ) 𝑦 ) ∈ 𝐷 )
11 1 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
12 11 ancoms ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐴 ∈ Ring )
13 eqid ( 1r𝐴 ) = ( 1r𝐴 )
14 eqid ( .r𝐴 ) = ( .r𝐴 )
15 2 13 14 issubrg2 ( 𝐴 ∈ Ring → ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) ↔ ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) ∧ ( 1r𝐴 ) ∈ 𝐷 ∧ ∀ 𝑥𝐷𝑦𝐷 ( 𝑥 ( .r𝐴 ) 𝑦 ) ∈ 𝐷 ) ) )
16 12 15 syl ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) ↔ ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) ∧ ( 1r𝐴 ) ∈ 𝐷 ∧ ∀ 𝑥𝐷𝑦𝐷 ( 𝑥 ( .r𝐴 ) 𝑦 ) ∈ 𝐷 ) ) )
17 5 7 10 16 mpbir3and ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )