Theorem rlmsub

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

	Ref	Expression
Assertion	rlmsub	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ ( ringLMod ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rlmbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
2	1	a1i	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
3		rlmplusg	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
4	3	a1i	⊢ ( ⊤ → ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) ) )
5	2 4	grpsubpropd	⊢ ( ⊤ → ( -g ‘ 𝑅 ) = ( -g ‘ ( ringLMod ‘ 𝑅 ) ) )
6	5	mptru	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ ( ringLMod ‘ 𝑅 ) )