Theorem matsubg

Description: The matrix ring has the same addition as its underlying group. (Contributed by AV, 2-Aug-2019)

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

Proof

Step	Hyp	Ref	Expression
1		matsubg.a	$$⊢A=N\mathrm{Mat}R$$
2		matsubg.g	$$⊢G=R\mathrm{freeLMod}\left(N\times N\right)$$
3	1 2	matbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\mathrm{Base}}_G={\mathrm{Base}}_A$$
4	1 2	matplusg	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {+}_G={+}_A$$
5	3 4	grpsubpropd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {-}_G={-}_A$$