Metamath Proof Explorer

Theorem scmatid

Description: The identity matrix is a scalar matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 18-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 scmatid 
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. S )

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 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
7 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
8 2 7 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
9 6 8 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B )
10 1 matsca2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
11 10 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` A ) = R )
12 11 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` ( Scalar ` A ) ) = ( 1r ` R ) )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
15 13 14 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
16 15 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` R ) e. ( Base ` R ) )
17 12 16 eqeltrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` ( Scalar ` A ) ) e. ( Base ` R ) )
18 oveq1 
 |-  ( c = ( 1r ` ( Scalar ` A ) ) -> ( c ( .s ` A ) ( 1r ` A ) ) = ( ( 1r ` ( Scalar ` A ) ) ( .s ` A ) ( 1r ` A ) ) )
19 18 eqeq2d 
 |-  ( c = ( 1r ` ( Scalar ` A ) ) -> ( ( 1r ` A ) = ( c ( .s ` A ) ( 1r ` A ) ) <-> ( 1r ` A ) = ( ( 1r ` ( Scalar ` A ) ) ( .s ` A ) ( 1r ` A ) ) ) )
20 19 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ c = ( 1r ` ( Scalar ` A ) ) ) -> ( ( 1r ` A ) = ( c ( .s ` A ) ( 1r ` A ) ) <-> ( 1r ` A ) = ( ( 1r ` ( Scalar ` A ) ) ( .s ` A ) ( 1r ` A ) ) ) )
21 1 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
22 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
23 eqid 
 |-  ( .s ` A ) = ( .s ` A )
24 eqid 
 |-  ( 1r ` ( Scalar ` A ) ) = ( 1r ` ( Scalar ` A ) )
25 2 22 23 24 lmodvs1 
 |-  ( ( A e. LMod /\ ( 1r ` A ) e. B ) -> ( ( 1r ` ( Scalar ` A ) ) ( .s ` A ) ( 1r ` A ) ) = ( 1r ` A ) )
26 21 9 25 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( 1r ` ( Scalar ` A ) ) ( .s ` A ) ( 1r ` A ) ) = ( 1r ` A ) )
27 26 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( ( 1r ` ( Scalar ` A ) ) ( .s ` A ) ( 1r ` A ) ) )
28 17 20 27 rspcedvd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> E. c e. ( Base ` R ) ( 1r ` A ) = ( c ( .s ` A ) ( 1r ` A ) ) )
29 13 1 2 7 23 5 scmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( 1r ` A ) e. S <-> ( ( 1r ` A ) e. B /\ E. c e. ( Base ` R ) ( 1r ` A ) = ( c ( .s ` A ) ( 1r ` A ) ) ) ) )
30 9 28 29 mpbir2and 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. S )