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 ) )