Metamath Proof Explorer


Theorem lmodvnegcl

Description: Closure of vector negative. (Contributed by NM, 18-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmodvnegcl.v V=BaseW
lmodvnegcl.n N=invgW
Assertion lmodvnegcl WLModXVNXV

Proof

Step Hyp Ref Expression
1 lmodvnegcl.v V=BaseW
2 lmodvnegcl.n N=invgW
3 lmodgrp WLModWGrp
4 1 2 grpinvcl WGrpXVNXV
5 3 4 sylan WLModXVNXV