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 )