Theorem mat1bas

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

	Ref	Expression
Hypotheses	mat1bas.a	$$⊢A=N\mathrm{Mat}R$$
	mat1bas.b	$$⊢B={\mathrm{Base}}_A$$
	mat1bas.i	$$⊢\underset{\dot{}}{1}=1_{\left(N\mathrm{Mat}R\right)}$$
Assertion	mat1bas	$$⊢\left(R\in \mathrm{Ring}\wedge N\in \mathrm{Fin}\right)\to \underset{\dot{}}{1}\in B$$

Proof

Step	Hyp	Ref	Expression
1		mat1bas.a	$$⊢A=N\mathrm{Mat}R$$
2		mat1bas.b	$$⊢B={\mathrm{Base}}_A$$
3		mat1bas.i	$$⊢\underset{\dot{}}{1}=1_{\left(N\mathrm{Mat}R\right)}$$
4		eqid	$$⊢N\mathrm{Mat}R=N\mathrm{Mat}R$$
5	4	matring	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to N\mathrm{Mat}R\in \mathrm{Ring}$$
6	5	ancoms	$$⊢\left(R\in \mathrm{Ring}\wedge N\in \mathrm{Fin}\right)\to N\mathrm{Mat}R\in \mathrm{Ring}$$
7	1	fveq2i	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
8	2 7	eqtri	$$⊢B={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
9	8 3	ringidcl	$$⊢N\mathrm{Mat}R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
10	6 9	syl	$$⊢\left(R\in \mathrm{Ring}\wedge N\in \mathrm{Fin}\right)\to \underset{\dot{}}{1}\in B$$