Metamath Proof Explorer

Theorem scmatsgrp1

Description: The set of scalar matrices is a subgroup of the group/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 scmatsgrp1 
|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` 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 scmatdmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( x e. S -> x e. D ) )
9 8 ssrdv 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S C_ D )
10 1 2 4 6 dmatsgrp 
 |-  ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubGrp ` A ) )
11 10 ancoms 
 |-  ( ( N e. Fin /\ R e. Ring ) -> D e. ( SubGrp ` A ) )
12 7 subgbas 
 |-  ( D e. ( SubGrp ` A ) -> D = ( Base ` C ) )
13 12 eqcomd 
 |-  ( D e. ( SubGrp ` A ) -> ( Base ` C ) = D )
14 11 13 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` C ) = D )
15 9 14 sseqtrrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S C_ ( Base ` C ) )
16 1 2 3 4 5 scmatid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. S )
17 16 ne0d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S =/= (/) )
18 11 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> D e. ( SubGrp ` A ) )
19 8 com12 
 |-  ( x e. S -> ( ( N e. Fin /\ R e. Ring ) -> x e. D ) )
20 19 adantr 
 |-  ( ( x e. S /\ y e. S ) -> ( ( N e. Fin /\ R e. Ring ) -> x e. D ) )
21 20 impcom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> x e. D )
22 1 2 3 4 5 6 scmatdmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y e. S -> y e. D ) )
23 22 a1d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( x e. S -> ( y e. S -> y e. D ) ) )
24 23 imp32 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> y e. D )
25 eqid 
 |-  ( -g ` A ) = ( -g ` A )
26 eqid 
 |-  ( -g ` C ) = ( -g ` C )
27 25 7 26 subgsub 
 |-  ( ( D e. ( SubGrp ` A ) /\ x e. D /\ y e. D ) -> ( x ( -g ` A ) y ) = ( x ( -g ` C ) y ) )
28 27 eqcomd 
 |-  ( ( D e. ( SubGrp ` A ) /\ x e. D /\ y e. D ) -> ( x ( -g ` C ) y ) = ( x ( -g ` A ) y ) )
29 18 21 24 28 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( -g ` C ) y ) = ( x ( -g ` A ) y ) )
30 1 2 3 4 5 scmatsubcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( -g ` A ) y ) e. S )
31 29 30 eqeltrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( -g ` C ) y ) e. S )
32 31 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( -g ` C ) y ) e. S )
33 1 2 4 6 dmatsrng 
 |-  ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubRing ` A ) )
34 33 ancoms 
 |-  ( ( N e. Fin /\ R e. Ring ) -> D e. ( SubRing ` A ) )
35 7 subrgring 
 |-  ( D e. ( SubRing ` A ) -> C e. Ring )
36 34 35 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
37 ringgrp 
 |-  ( C e. Ring -> C e. Grp )
38 eqid 
 |-  ( Base ` C ) = ( Base ` C )
39 38 26 issubg4 
 |-  ( C e. Grp -> ( S e. ( SubGrp ` C ) <-> ( S C_ ( Base ` C ) /\ S =/= (/) /\ A. x e. S A. y e. S ( x ( -g ` C ) y ) e. S ) ) )
40 36 37 39 3syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( S e. ( SubGrp ` C ) <-> ( S C_ ( Base ` C ) /\ S =/= (/) /\ A. x e. S A. y e. S ( x ( -g ` C ) y ) e. S ) ) )
41 15 17 32 40 mpbir3and 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )