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={\mathrm{Base}}_W$$
	lmodvnegcl.n	$$⊢N={inv}_g\left(W\right)$$
Assertion	lmodvnegcl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(X\right)\in V$$

Proof

Step	Hyp	Ref	Expression
1		lmodvnegcl.v	$$⊢V={\mathrm{Base}}_W$$
2		lmodvnegcl.n	$$⊢N={inv}_g\left(W\right)$$
3		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
4	1 2	grpinvcl	$$⊢\left(W\in \mathrm{Grp}\wedge X\in V\right)\to N\left(X\right)\in V$$
5	3 4	sylan	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(X\right)\in V$$