Theorem matbas2i

Description: A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015)

	Ref	Expression
Hypotheses	matbas2.a	$$⊢A=N\mathrm{Mat}R$$
	matbas2.k	$$⊢K={\mathrm{Base}}_R$$
	matbas2i.b	$$⊢B={\mathrm{Base}}_A$$
Assertion	matbas2i	$$⊢M\in B\to M\in \left(K^{\left(N\times N\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		matbas2.a	$$⊢A=N\mathrm{Mat}R$$
2		matbas2.k	$$⊢K={\mathrm{Base}}_R$$
3		matbas2i.b	$$⊢B={\mathrm{Base}}_A$$
4		id	$$⊢M\in B\to M\in B$$
5	4 3	eleqtrdi	$$⊢M\in B\to M\in {\mathrm{Base}}_A$$
6	1 3	matrcl	$$⊢M\in B\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)$$
7	1 2	matbas2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to K^{\left(N\times N\right)}={\mathrm{Base}}_A$$
8	6 7	syl	$$⊢M\in B\to K^{\left(N\times N\right)}={\mathrm{Base}}_A$$
9	5 8	eleqtrrd	$$⊢M\in B\to M\in \left(K^{\left(N\times N\right)}\right)$$