Theorem rlmsub

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

	Ref	Expression
Assertion	rlmsub	|- ( -g ` R ) = ( -g ` ( ringLMod ` R ) )

Proof

Step	Hyp	Ref	Expression
1		rlmbas	|- ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
2	1	a1i	|- ( T. -> ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) )
3		rlmplusg	|- ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
4	3	a1i	|- ( T. -> ( +g ` R ) = ( +g ` ( ringLMod ` R ) ) )
5	2 4	grpsubpropd	|- ( T. -> ( -g ` R ) = ( -g ` ( ringLMod ` R ) ) )
6	5	mptru	|- ( -g ` R ) = ( -g ` ( ringLMod ` R ) )