Theorem mat0

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