Metamath Proof Explorer

Theorem mat0scmat

Description: The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat , also a diagonal matrix). (Contributed by AV, 21-Dec-2019)

Ref Expression
Assertion mat0scmat 
|- ( R e. Ring -> (/) e. ( (/) ScMat R ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 snid 
 |-  (/) e. { (/) }
3 mat0dimbas0 
 |-  ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } )
4 2 3 eleqtrrid 
 |-  ( R e. Ring -> (/) e. ( Base ` ( (/) Mat R ) ) )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
7 5 6 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
8 oveq1 
 |-  ( c = ( 1r ` R ) -> ( c ( .s ` ( (/) Mat R ) ) (/) ) = ( ( 1r ` R ) ( .s ` ( (/) Mat R ) ) (/) ) )
9 8 eqeq2d 
 |-  ( c = ( 1r ` R ) -> ( (/) = ( c ( .s ` ( (/) Mat R ) ) (/) ) <-> (/) = ( ( 1r ` R ) ( .s ` ( (/) Mat R ) ) (/) ) ) )
10 9 adantl 
 |-  ( ( R e. Ring /\ c = ( 1r ` R ) ) -> ( (/) = ( c ( .s ` ( (/) Mat R ) ) (/) ) <-> (/) = ( ( 1r ` R ) ( .s ` ( (/) Mat R ) ) (/) ) ) )
11 eqid 
 |-  ( (/) Mat R ) = ( (/) Mat R )
12 11 mat0dimscm 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .s ` ( (/) Mat R ) ) (/) ) = (/) )
13 7 12 mpdan 
 |-  ( R e. Ring -> ( ( 1r ` R ) ( .s ` ( (/) Mat R ) ) (/) ) = (/) )
14 13 eqcomd 
 |-  ( R e. Ring -> (/) = ( ( 1r ` R ) ( .s ` ( (/) Mat R ) ) (/) ) )
15 7 10 14 rspcedvd 
 |-  ( R e. Ring -> E. c e. ( Base ` R ) (/) = ( c ( .s ` ( (/) Mat R ) ) (/) ) )
16 11 mat0dimid 
 |-  ( R e. Ring -> ( 1r ` ( (/) Mat R ) ) = (/) )
17 16 oveq2d 
 |-  ( R e. Ring -> ( c ( .s ` ( (/) Mat R ) ) ( 1r ` ( (/) Mat R ) ) ) = ( c ( .s ` ( (/) Mat R ) ) (/) ) )
18 17 eqeq2d 
 |-  ( R e. Ring -> ( (/) = ( c ( .s ` ( (/) Mat R ) ) ( 1r ` ( (/) Mat R ) ) ) <-> (/) = ( c ( .s ` ( (/) Mat R ) ) (/) ) ) )
19 18 rexbidv 
 |-  ( R e. Ring -> ( E. c e. ( Base ` R ) (/) = ( c ( .s ` ( (/) Mat R ) ) ( 1r ` ( (/) Mat R ) ) ) <-> E. c e. ( Base ` R ) (/) = ( c ( .s ` ( (/) Mat R ) ) (/) ) ) )
20 15 19 mpbird 
 |-  ( R e. Ring -> E. c e. ( Base ` R ) (/) = ( c ( .s ` ( (/) Mat R ) ) ( 1r ` ( (/) Mat R ) ) ) )
21 0fin 
 |-  (/) e. Fin
22 eqid 
 |-  ( Base ` ( (/) Mat R ) ) = ( Base ` ( (/) Mat R ) )
23 eqid 
 |-  ( 1r ` ( (/) Mat R ) ) = ( 1r ` ( (/) Mat R ) )
24 eqid 
 |-  ( .s ` ( (/) Mat R ) ) = ( .s ` ( (/) Mat R ) )
25 eqid 
 |-  ( (/) ScMat R ) = ( (/) ScMat R )
26 5 11 22 23 24 25 scmatel 
 |-  ( ( (/) e. Fin /\ R e. Ring ) -> ( (/) e. ( (/) ScMat R ) <-> ( (/) e. ( Base ` ( (/) Mat R ) ) /\ E. c e. ( Base ` R ) (/) = ( c ( .s ` ( (/) Mat R ) ) ( 1r ` ( (/) Mat R ) ) ) ) ) )
27 21 26 mpan 
 |-  ( R e. Ring -> ( (/) e. ( (/) ScMat R ) <-> ( (/) e. ( Base ` ( (/) Mat R ) ) /\ E. c e. ( Base ` R ) (/) = ( c ( .s ` ( (/) Mat R ) ) ( 1r ` ( (/) Mat R ) ) ) ) ) )
28 4 20 27 mpbir2and 
 |-  ( R e. Ring -> (/) e. ( (/) ScMat R ) )