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	|- ( invg ` R ) = ( invg ` ( ringLMod ` R ) )

Proof

Step	Hyp	Ref	Expression
1		eqidd	|- ( T. -> ( Base ` R ) = ( Base ` R ) )
2		rlmbas	|- ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
3	2	a1i	|- ( T. -> ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) )
4		rlmplusg	|- ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
5	4	a1i	|- ( ( T. /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( +g ` R ) = ( +g ` ( ringLMod ` R ) ) )
6	5	oveqd	|- ( ( T. /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` ( ringLMod ` R ) ) y ) )
7	1 3 6	grpinvpropd	|- ( T. -> ( invg ` R ) = ( invg ` ( ringLMod ` R ) ) )
8	7	mptru	|- ( invg ` R ) = ( invg ` ( ringLMod ` R ) )