Theorem rlmsub

Description: Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Assertion	rlmsub	$$⊢{-}_R={-}_{\mathrm{ringLMod}\left(R\right)}$$

Proof

Step	Hyp	Ref	Expression
1		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
2	1	a1i	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
3		rlmplusg	$$⊢{+}_R={+}_{\mathrm{ringLMod}\left(R\right)}$$
4	3	a1i	$$⊢\top \to {+}_R={+}_{\mathrm{ringLMod}\left(R\right)}$$
5	2 4	grpsubpropd	$$⊢\top \to {-}_R={-}_{\mathrm{ringLMod}\left(R\right)}$$
6	5	mptru	$$⊢{-}_R={-}_{\mathrm{ringLMod}\left(R\right)}$$