Metamath Proof Explorer

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 \in Fin \land R \in V) \to K^{(N \times N)} = {Base}_{A}$

Proof

Step	Hyp	Ref	Expression
1		matbas2.a	$⊢ A = N Mat R$
2		matbas2.k	$⊢ K = {Base}_{R}$
3		xpfi	$⊢ (N \in Fin \land N \in Fin) \to N \times N \in Fin$
4	3	anidms	$⊢ N \in Fin \to N \times N \in Fin$
5	4	anim1ci	$⊢ (N \in Fin \land R \in V) \to (R \in V \land N \times N \in Fin)$
6		eqid	$⊢ R freeLMod (N \times N) = R freeLMod (N \times N)$
7	6 2	frlmfibas	$⊢ (R \in V \land N \times N \in Fin) \to K^{(N \times N)} = {Base}_{(R freeLMod (N \times N))}$
8	5 7	syl	$⊢ (N \in Fin \land R \in V) \to K^{(N \times N)} = {Base}_{(R freeLMod (N \times N))}$
9	1 6	matbas	$⊢ (N \in Fin \land R \in V) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
10	8 9	eqtrd	$⊢ (N \in Fin \land R \in V) \to K^{(N \times N)} = {Base}_{A}$