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. = ( 0g ` R )
scmatid.s 
|- S = ( N ScMat R )
Assertion scmatsrng 
|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( 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. = ( 0g ` R )
5 scmatid.s 
 |-  S = ( N ScMat R )
6 1 2 3 4 5 scmatsgrp 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` A ) )
7 1 2 3 4 5 scmatid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. S )
8 1 2 3 4 5 scmatmulcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( .r ` A ) y ) e. S )
9 8 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( .r ` A ) y ) e. S )
10 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
11 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
12 eqid 
 |-  ( .r ` A ) = ( .r ` A )
13 2 11 12 issubrg2 
 |-  ( A e. Ring -> ( S e. ( SubRing ` A ) <-> ( S e. ( SubGrp ` A ) /\ ( 1r ` A ) e. S /\ A. x e. S A. y e. S ( x ( .r ` A ) y ) e. S ) ) )
14 10 13 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( S e. ( SubRing ` A ) <-> ( S e. ( SubGrp ` A ) /\ ( 1r ` A ) e. S /\ A. x e. S A. y e. S ( x ( .r ` A ) y ) e. S ) ) )
15 6 7 9 14 mpbir3and 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubRing ` A ) )