Theorem matvsca

Description: The matrix ring has the same scalar multiplication 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	matvsca	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\cdot }_G={\cdot }_A$$

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		eqid	$$⊢R\mathrm{maMul}⟨N,N,N⟩=R\mathrm{maMul}⟨N,N,N⟩$$
4	1 2 3	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⟩⟩$$
5	4	fveq2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\cdot }_A={\cdot }_{\left(G\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},R\mathrm{maMul}⟨N,N,N⟩⟩\right)}$$
6		vscaid	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
7		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
8		3re	$$⊢3\in ℝ$$
9		3lt6	$$⊢3<6$$
10	8 9	gtneii	$$⊢6\ne 3$$
11		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
12	10 11	neeqtrri	$$⊢6\ne {\cdot }_{\mathrm{ndx}}$$
13	7 12	eqnetri	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
14	6 13	setsnid	$$⊢{\cdot }_G={\cdot }_{\left(G\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},R\mathrm{maMul}⟨N,N,N⟩⟩\right)}$$
15	5 14	syl6reqr	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\cdot }_G={\cdot }_A$$