Metamath Proof Explorer

Theorem mat0dimid

Description: The identity of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019)

Ref Expression
Hypothesis mat0dim.a 
|- A = ( (/) Mat R )
Assertion mat0dimid 
|- ( R e. Ring -> ( 1r ` A ) = (/) )

Proof

Step Hyp Ref Expression
1 mat0dim.a 
 |-  A = ( (/) Mat R )
2 0fin 
 |-  (/) e. Fin
3 1 matring 
 |-  ( ( (/) e. Fin /\ R e. Ring ) -> A e. Ring )
4 2 3 mpan 
 |-  ( R e. Ring -> A e. Ring )
5 eqid 
 |-  ( Base ` A ) = ( Base ` A )
6 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
7 5 6 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. ( Base ` A ) )
8 4 7 syl 
 |-  ( R e. Ring -> ( 1r ` A ) e. ( Base ` A ) )
9 1 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( (/) Mat R ) )
10 mat0dimbas0 
 |-  ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } )
11 9 10 syl5eq 
 |-  ( R e. Ring -> ( Base ` A ) = { (/) } )
12 11 eleq2d 
 |-  ( R e. Ring -> ( ( 1r ` A ) e. ( Base ` A ) <-> ( 1r ` A ) e. { (/) } ) )
13 elsni 
 |-  ( ( 1r ` A ) e. { (/) } -> ( 1r ` A ) = (/) )
14 12 13 syl6bi 
 |-  ( R e. Ring -> ( ( 1r ` A ) e. ( Base ` A ) -> ( 1r ` A ) = (/) ) )
15 8 14 mpd 
 |-  ( R e. Ring -> ( 1r ` A ) = (/) )