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} (R) = {inv}_{g} (ringLMod (R))$

Step	Hyp	Ref	Expression
1		eqidd	$⊢ ⊤ \to {Base}_{R} = {Base}_{R}$
2		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
3	2	a1i	$⊢ ⊤ \to {Base}_{R} = {Base}_{ringLMod (R)}$
4		rlmplusg	$⊢ +_{R} = +_{ringLMod (R)}$
5	4	a1i	$⊢ (⊤ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to +_{R} = +_{ringLMod (R)}$
6	5	oveqd	$⊢ (⊤ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x +_{R} y = x +_{ringLMod (R)} y$
7	1 3 6	grpinvpropd	$⊢ ⊤ \to {inv}_{g} (R) = {inv}_{g} (ringLMod (R))$
8	7	mptru	$⊢ {inv}_{g} (R) = {inv}_{g} (ringLMod (R))$

Metamath Proof Explorer