This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )