This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mat1bas

Description: The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019)

Ref Expression
Hypotheses mat1bas.a 
|- A = ( N Mat R )
mat1bas.b 
|- B = ( Base ` A )
mat1bas.i 
|- .1. = ( 1r ` ( N Mat R ) )
Assertion mat1bas 
|- ( ( R e. Ring /\ N e. Fin ) -> .1. e. B )

Proof

Step Hyp Ref Expression
1 mat1bas.a 
 |-  A = ( N Mat R )
2 mat1bas.b 
 |-  B = ( Base ` A )
3 mat1bas.i 
 |-  .1. = ( 1r ` ( N Mat R ) )
4 eqid 
 |-  ( N Mat R ) = ( N Mat R )
5 4 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N Mat R ) e. Ring )
6 5 ancoms 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( N Mat R ) e. Ring )
7 1 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
8 2 7 eqtri 
 |-  B = ( Base ` ( N Mat R ) )
9 8 3 ringidcl 
 |-  ( ( N Mat R ) e. Ring -> .1. e. B )
10 6 9 syl 
 |-  ( ( R e. Ring /\ N e. Fin ) -> .1. e. B )