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 ) = (/) )