Theorem matsca2

Description: The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypothesis	matsca2.a	$$⊢A=N\mathrm{Mat}R$$
Assertion	matsca2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to R=\mathrm{Scalar}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		matsca2.a	$$⊢A=N\mathrm{Mat}R$$
2		xpfi	$$⊢\left(N\in \mathrm{Fin}\wedge N\in \mathrm{Fin}\right)\to N\times N\in \mathrm{Fin}$$
3	2	anidms	$$⊢N\in \mathrm{Fin}\to N\times N\in \mathrm{Fin}$$
4		eqid	$$⊢R\mathrm{freeLMod}\left(N\times N\right)=R\mathrm{freeLMod}\left(N\times N\right)$$
5	4	frlmsca	$$⊢\left(R\in V\wedge N\times N\in \mathrm{Fin}\right)\to R=\mathrm{Scalar}\left(R\mathrm{freeLMod}\left(N\times N\right)\right)$$
6	5	ancoms	$$⊢\left(N\times N\in \mathrm{Fin}\wedge R\in V\right)\to R=\mathrm{Scalar}\left(R\mathrm{freeLMod}\left(N\times N\right)\right)$$
7	3 6	sylan	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to R=\mathrm{Scalar}\left(R\mathrm{freeLMod}\left(N\times N\right)\right)$$
8	1 4	matsca	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \mathrm{Scalar}\left(R\mathrm{freeLMod}\left(N\times N\right)\right)=\mathrm{Scalar}\left(A\right)$$
9	7 8	eqtrd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to R=\mathrm{Scalar}\left(A\right)$$