Metamath Proof Explorer

Theorem scmatsgrp

Description: The set of scalar matrices is a subgroup of the matrix group/algebra. (Contributed by AV, 20-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 scmatsgrp 
|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` 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 5 scmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( z e. S -> z e. B ) )
7 6 ssrdv 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S C_ B )
8 1 2 3 4 5 scmatid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. S )
9 8 ne0d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S =/= (/) )
10 1 2 3 4 5 scmatsubcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( -g ` A ) y ) e. S )
11 10 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( -g ` A ) y ) e. S )
12 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
13 ringgrp 
 |-  ( A e. Ring -> A e. Grp )
14 eqid 
 |-  ( -g ` A ) = ( -g ` A )
15 2 14 issubg4 
 |-  ( A e. Grp -> ( S e. ( SubGrp ` A ) <-> ( S C_ B /\ S =/= (/) /\ A. x e. S A. y e. S ( x ( -g ` A ) y ) e. S ) ) )
16 12 13 15 3syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( S e. ( SubGrp ` A ) <-> ( S C_ B /\ S =/= (/) /\ A. x e. S A. y e. S ( x ( -g ` A ) y ) e. S ) ) )
17 7 9 11 16 mpbir3and 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` A ) )