Theorem matbas2i

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

	Ref	Expression
Hypotheses	matbas2.a	|- A = ( N Mat R )
	matbas2.k	|- K = ( Base ` R )
	matbas2i.b	|- B = ( Base ` A )
Assertion	matbas2i	|- ( M e. B -> M e. ( K ^m ( N X. N ) ) )

Proof

Step	Hyp	Ref	Expression
1		matbas2.a	|- A = ( N Mat R )
2		matbas2.k	|- K = ( Base ` R )
3		matbas2i.b	|- B = ( Base ` A )
4		id	|- ( M e. B -> M e. B )
5	4 3	eleqtrdi	|- ( M e. B -> M e. ( Base ` A ) )
6	1 3	matrcl	|- ( M e. B -> ( N e. Fin /\ R e. _V ) )
7	1 2	matbas2	|- ( ( N e. Fin /\ R e. _V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
8	6 7	syl	|- ( M e. B -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
9	5 8	eleqtrrd	|- ( M e. B -> M e. ( K ^m ( N X. N ) ) )