Theorem matbas2

Description: The base set of the matrix ring as a set exponential. (Contributed by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 16-Dec-2018)

	Ref	Expression
Hypotheses	matbas2.a	|- A = ( N Mat R )
	matbas2.k	|- K = ( Base ` R )
Assertion	matbas2	|- ( ( N e. Fin /\ R e. V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )

Proof

Step	Hyp	Ref	Expression
1		matbas2.a	|- A = ( N Mat R )
2		matbas2.k	|- K = ( Base ` R )
3		xpfi	|- ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
4	3	anidms	|- ( N e. Fin -> ( N X. N ) e. Fin )
5	4	anim1ci	|- ( ( N e. Fin /\ R e. V ) -> ( R e. V /\ ( N X. N ) e. Fin ) )
6		eqid	|- ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
7	6 2	frlmfibas	|- ( ( R e. V /\ ( N X. N ) e. Fin ) -> ( K ^m ( N X. N ) ) = ( Base ` ( R freeLMod ( N X. N ) ) ) )
8	5 7	syl	|- ( ( N e. Fin /\ R e. V ) -> ( K ^m ( N X. N ) ) = ( Base ` ( R freeLMod ( N X. N ) ) ) )
9	1 6	matbas	|- ( ( N e. Fin /\ R e. V ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
10	8 9	eqtrd	|- ( ( N e. Fin /\ R e. V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )