Metamath Proof Explorer

Theorem mat0dim0

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

Ref Expression
Hypothesis mat0dim.a 
|- A = ( (/) Mat R )
Assertion mat0dim0 
|- ( R e. Ring -> ( 0g ` A ) = (/) )

Proof

Step Hyp Ref Expression
1 mat0dim.a 
 |-  A = ( (/) Mat R )
2 0fi 
 |-  (/) e. Fin
3 1 matring 
 |-  ( ( (/) e. Fin /\ R e. Ring ) -> A e. Ring )
4 2 3 mpan 
 |-  ( R e. Ring -> A e. Ring )
5 ringgrp 
 |-  ( A e. Ring -> A e. Grp )
6 eqid 
 |-  ( Base ` A ) = ( Base ` A )
7 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
8 6 7 grpidcl 
 |-  ( A e. Grp -> ( 0g ` A ) e. ( Base ` A ) )
9 4 5 8 3syl 
 |-  ( R e. Ring -> ( 0g ` A ) e. ( Base ` A ) )
10 1 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( (/) Mat R ) )
11 mat0dimbas0 
 |-  ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } )
12 10 11 eqtrid 
 |-  ( R e. Ring -> ( Base ` A ) = { (/) } )
13 12 eleq2d 
 |-  ( R e. Ring -> ( ( 0g ` A ) e. ( Base ` A ) <-> ( 0g ` A ) e. { (/) } ) )
14 elsni 
 |-  ( ( 0g ` A ) e. { (/) } -> ( 0g ` A ) = (/) )
15 13 14 biimtrdi 
 |-  ( R e. Ring -> ( ( 0g ` A ) e. ( Base ` A ) -> ( 0g ` A ) = (/) ) )
16 9 15 mpd 
 |-  ( R e. Ring -> ( 0g ` A ) = (/) )