Theorem rlmvneg

Description: Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014) (Revised by Mario Carneiro, 5-Jun-2015)

	Ref	Expression
Assertion	rlmvneg	$$⊢{inv}_g\left(R\right)={inv}_g\left(\mathrm{ringLMod}\left(R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_R$$
2		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
3	2	a1i	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
4		rlmplusg	$$⊢{+}_R={+}_{\mathrm{ringLMod}\left(R\right)}$$
5	4	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to {+}_R={+}_{\mathrm{ringLMod}\left(R\right)}$$
6	5	oveqd	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to x{+}_{R}y=x{+}_{\mathrm{ringLMod}\left(R\right)}y$$
7	1 3 6	grpinvpropd	$$⊢\top \to {inv}_g\left(R\right)={inv}_g\left(\mathrm{ringLMod}\left(R\right)\right)$$
8	7	mptru	$$⊢{inv}_g\left(R\right)={inv}_g\left(\mathrm{ringLMod}\left(R\right)\right)$$