Metamath Proof Explorer


Theorem lssvnegcl

Description: Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014)

Ref Expression
Hypotheses lssvnegcl.s S=LSubSpW
lssvnegcl.n N=invgW
Assertion lssvnegcl WLModUSXUNXU

Proof

Step Hyp Ref Expression
1 lssvnegcl.s S=LSubSpW
2 lssvnegcl.n N=invgW
3 eqid BaseW=BaseW
4 3 1 lssel USXUXBaseW
5 eqid ScalarW=ScalarW
6 eqid W=W
7 eqid 1ScalarW=1ScalarW
8 eqid invgScalarW=invgScalarW
9 3 2 5 6 7 8 lmodvneg1 WLModXBaseWinvgScalarW1ScalarWWX=NX
10 4 9 sylan2 WLModUSXUinvgScalarW1ScalarWWX=NX
11 10 3impb WLModUSXUinvgScalarW1ScalarWWX=NX
12 simp1 WLModUSXUWLMod
13 simp2 WLModUSXUUS
14 5 lmodring WLModScalarWRing
15 14 3ad2ant1 WLModUSXUScalarWRing
16 ringgrp ScalarWRingScalarWGrp
17 15 16 syl WLModUSXUScalarWGrp
18 eqid BaseScalarW=BaseScalarW
19 18 7 ringidcl ScalarWRing1ScalarWBaseScalarW
20 15 19 syl WLModUSXU1ScalarWBaseScalarW
21 18 8 grpinvcl ScalarWGrp1ScalarWBaseScalarWinvgScalarW1ScalarWBaseScalarW
22 17 20 21 syl2anc WLModUSXUinvgScalarW1ScalarWBaseScalarW
23 simp3 WLModUSXUXU
24 5 6 18 1 lssvscl WLModUSinvgScalarW1ScalarWBaseScalarWXUinvgScalarW1ScalarWWXU
25 12 13 22 23 24 syl22anc WLModUSXUinvgScalarW1ScalarWWXU
26 11 25 eqeltrrd WLModUSXUNXU