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
|- A = ( N Mat R )
dmatid.b
|- B = ( Base ` A )
dmatid.0
|- .0. = ( 0g ` R )
dmatid.d
|- D = ( N DMat R )
Assertion dmatsrng
|- ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubRing ` A ) )

Proof

Step Hyp Ref Expression
1 dmatid.a
 |-  A = ( N Mat R )
2 dmatid.b
 |-  B = ( Base ` A )
3 dmatid.0
 |-  .0. = ( 0g ` R )
4 dmatid.d
 |-  D = ( N DMat R )
5 1 2 3 4 dmatsgrp
 |-  ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubGrp ` A ) )
6 1 2 3 4 dmatid
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. D )
7 6 ancoms
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( 1r ` A ) e. D )
8 1 2 3 4 dmatmulcl
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. D /\ y e. D ) ) -> ( x ( .r ` A ) y ) e. D )
9 8 ralrimivva
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. D A. y e. D ( x ( .r ` A ) y ) e. D )
10 9 ancoms
 |-  ( ( R e. Ring /\ N e. Fin ) -> A. x e. D A. y e. D ( x ( .r ` A ) y ) e. D )
11 1 matring
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
12 11 ancoms
 |-  ( ( R e. Ring /\ N e. Fin ) -> A e. Ring )
13 eqid
 |-  ( 1r ` A ) = ( 1r ` A )
14 eqid
 |-  ( .r ` A ) = ( .r ` A )
15 2 13 14 issubrg2
 |-  ( A e. Ring -> ( D e. ( SubRing ` A ) <-> ( D e. ( SubGrp ` A ) /\ ( 1r ` A ) e. D /\ A. x e. D A. y e. D ( x ( .r ` A ) y ) e. D ) ) )
16 12 15 syl
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( D e. ( SubRing ` A ) <-> ( D e. ( SubGrp ` A ) /\ ( 1r ` A ) e. D /\ A. x e. D A. y e. D ( x ( .r ` A ) y ) e. D ) ) )
17 5 7 10 16 mpbir3and
 |-  ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubRing ` A ) )