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 invgR=invgringLModR

Proof

Step Hyp Ref Expression
1 eqidd BaseR=BaseR
2 rlmbas BaseR=BaseringLModR
3 2 a1i BaseR=BaseringLModR
4 rlmplusg +R=+ringLModR
5 4 a1i xBaseRyBaseR+R=+ringLModR
6 5 oveqd xBaseRyBaseRx+Ry=x+ringLModRy
7 1 3 6 grpinvpropd invgR=invgringLModR
8 7 mptru invgR=invgringLModR