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. = ( 0g ` R )
scmatid.s 
|- S = ( N ScMat R )
scmatsgrp1.d 
|- D = ( N DMat R )
scmatsgrp1.c 
|- C = ( A |`s D )
Assertion scmatsrng1 
|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( 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. = ( 0g ` R )
5 scmatid.s 
 |-  S = ( N ScMat R )
6 scmatsgrp1.d 
 |-  D = ( N DMat R )
7 scmatsgrp1.c 
 |-  C = ( A |`s D )
8 1 2 3 4 5 6 7 scmatsgrp1 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )
9 1 2 4 6 dmatsrng 
 |-  ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubRing ` A ) )
10 9 ancoms 
 |-  ( ( N e. Fin /\ R e. Ring ) -> D e. ( SubRing ` A ) )
11 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
12 7 11 subrg1 
 |-  ( D e. ( SubRing ` A ) -> ( 1r ` A ) = ( 1r ` C ) )
13 10 12 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( 1r ` C ) )
14 13 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) = ( 1r ` A ) )
15 1 2 3 4 5 scmatid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. S )
16 14 15 eqeltrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. S )
17 eqid 
 |-  ( .r ` A ) = ( .r ` A )
18 7 17 ressmulr 
 |-  ( D e. ( SubRing ` A ) -> ( .r ` A ) = ( .r ` C ) )
19 10 18 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( .r ` A ) = ( .r ` C ) )
20 19 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( .r ` C ) = ( .r ` A ) )
21 20 oveqdr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( .r ` C ) y ) = ( x ( .r ` A ) y ) )
22 1 2 3 4 5 scmatmulcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( .r ` A ) y ) e. S )
23 21 22 eqeltrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( .r ` C ) y ) e. S )
24 23 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S )
25 7 subrgring 
 |-  ( D e. ( SubRing ` A ) -> C e. Ring )
26 eqid 
 |-  ( Base ` C ) = ( Base ` C )
27 eqid 
 |-  ( 1r ` C ) = ( 1r ` C )
28 eqid 
 |-  ( .r ` C ) = ( .r ` C )
29 26 27 28 issubrg2 
 |-  ( C e. Ring -> ( S e. ( SubRing ` C ) <-> ( S e. ( SubGrp ` C ) /\ ( 1r ` C ) e. S /\ A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S ) ) )
30 10 25 29 3syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( S e. ( SubRing ` C ) <-> ( S e. ( SubGrp ` C ) /\ ( 1r ` C ) e. S /\ A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S ) ) )
31 8 16 24 30 mpbir3and 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubRing ` C ) )