Metamath Proof Explorer

Theorem scmatlss

Description: The set of scalar matrices is a linear subspace of the matrix algebra. (Contributed by AV, 25-Dec-2019)

Ref Expression
Hypotheses scmatlss.a 
|- A = ( N Mat R )
scmatlss.s 
|- S = ( N ScMat R )
Assertion scmatlss 
|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( LSubSp ` A ) )

Proof

Step Hyp Ref Expression
1 scmatlss.a 
 |-  A = ( N Mat R )
2 scmatlss.s 
 |-  S = ( N ScMat R )
3 1 matsca2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
4 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` R ) )
5 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` A ) = ( Base ` A ) )
6 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( +g ` A ) = ( +g ` A ) )
7 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( .s ` A ) = ( .s ` A ) )
8 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( LSubSp ` A ) = ( LSubSp ` A ) )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 eqid 
 |-  ( Base ` A ) = ( Base ` A )
11 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
12 eqid 
 |-  ( .s ` A ) = ( .s ` A )
13 9 1 10 11 12 2 scmatval 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S = { m e. ( Base ` A ) | E. c e. ( Base ` R ) m = ( c ( .s ` A ) ( 1r ` A ) ) } )
14 ssrab2 
 |-  { m e. ( Base ` A ) | E. c e. ( Base ` R ) m = ( c ( .s ` A ) ( 1r ` A ) ) } C_ ( Base ` A )
15 13 14 eqsstrdi 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S C_ ( Base ` A ) )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 1 10 9 16 2 scmatid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. S )
18 17 ne0d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S =/= (/) )
19 9 1 2 12 smatvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. ( Base ` R ) /\ x e. S ) ) -> ( a ( .s ` A ) x ) e. S )
20 19 3adantr3 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. ( Base ` R ) /\ x e. S /\ y e. S ) ) -> ( a ( .s ` A ) x ) e. S )
21 simpr3 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. ( Base ` R ) /\ x e. S /\ y e. S ) ) -> y e. S )
22 20 21 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. ( Base ` R ) /\ x e. S /\ y e. S ) ) -> ( ( a ( .s ` A ) x ) e. S /\ y e. S ) )
23 1 10 9 16 2 scmataddcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( a ( .s ` A ) x ) e. S /\ y e. S ) ) -> ( ( a ( .s ` A ) x ) ( +g ` A ) y ) e. S )
24 22 23 syldan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. ( Base ` R ) /\ x e. S /\ y e. S ) ) -> ( ( a ( .s ` A ) x ) ( +g ` A ) y ) e. S )
25 3 4 5 6 7 8 15 18 24 islssd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( LSubSp ` A ) )