Theorem matinvg

Description: The matrix ring has the same additive inverse 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	matinvg	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {inv}_g\left(G\right)={inv}_g\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		eqidd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
4	1 2	matbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\mathrm{Base}}_G={\mathrm{Base}}_A$$
5	1 2	matplusg	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {+}_G={+}_A$$
6	5	oveqdr	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\right)\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{G}y=x{+}_{A}y$$
7	3 4 6	grpinvpropd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {inv}_g\left(G\right)={inv}_g\left(A\right)$$