Theorem matsca

Description: The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015)

	Ref	Expression
Hypotheses	matbas.a	$$⊢A=N\mathrm{Mat}R$$
	matbas.g	$$⊢G=R\mathrm{freeLMod}\left(N\times N\right)$$
Assertion	matsca	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \mathrm{Scalar}\left(G\right)=\mathrm{Scalar}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		matbas.a	$$⊢A=N\mathrm{Mat}R$$
2		matbas.g	$$⊢G=R\mathrm{freeLMod}\left(N\times N\right)$$
3		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
4		3re	$$⊢3\in ℝ$$
5		3lt5	$$⊢3<5$$
6	4 5	gtneii	$$⊢5\ne 3$$
7		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
8		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
9	7 8	neeq12i	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\leftrightarrow 5\ne 3$$
10	6 9	mpbir	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
11	3 10	setsnid	$$⊢\mathrm{Scalar}\left(G\right)=\mathrm{Scalar}\left(G\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},R\mathrm{maMul}⟨N,N,N⟩⟩\right)$$
12		eqid	$$⊢R\mathrm{maMul}⟨N,N,N⟩=R\mathrm{maMul}⟨N,N,N⟩$$
13	1 2 12	matval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to A=G\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},R\mathrm{maMul}⟨N,N,N⟩⟩$$
14	13	fveq2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \mathrm{Scalar}\left(A\right)=\mathrm{Scalar}\left(G\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},R\mathrm{maMul}⟨N,N,N⟩⟩\right)$$
15	11 14	eqtr4id	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \mathrm{Scalar}\left(G\right)=\mathrm{Scalar}\left(A\right)$$