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 โŠข ๐‘† = ( LSubSp โ€˜ ๐‘Š )
lssvnegcl.n โŠข ๐‘ = ( invg โ€˜ ๐‘Š )
Assertion lssvnegcl ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘ โ€˜ ๐‘‹ ) โˆˆ ๐‘ˆ )

Proof

Step Hyp Ref Expression
1 lssvnegcl.s โŠข ๐‘† = ( LSubSp โ€˜ ๐‘Š )
2 lssvnegcl.n โŠข ๐‘ = ( invg โ€˜ ๐‘Š )
3 eqid โŠข ( Base โ€˜ ๐‘Š ) = ( Base โ€˜ ๐‘Š )
4 3 1 lssel โŠข ( ( ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ๐‘‹ โˆˆ ( Base โ€˜ ๐‘Š ) )
5 eqid โŠข ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘Š )
6 eqid โŠข ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘Š )
7 eqid โŠข ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) )
8 eqid โŠข ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) )
9 3 2 5 6 7 8 lmodvneg1 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‹ โˆˆ ( Base โ€˜ ๐‘Š ) ) โ†’ ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‹ ) = ( ๐‘ โ€˜ ๐‘‹ ) )
10 4 9 sylan2 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) ) โ†’ ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‹ ) = ( ๐‘ โ€˜ ๐‘‹ ) )
11 10 3impb โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‹ ) = ( ๐‘ โ€˜ ๐‘‹ ) )
12 simp1 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ๐‘Š โˆˆ LMod )
13 simp2 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ๐‘ˆ โˆˆ ๐‘† )
14 5 lmodring โŠข ( ๐‘Š โˆˆ LMod โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring )
15 14 3ad2ant1 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring )
16 ringgrp โŠข ( ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Grp )
17 15 16 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Grp )
18 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) )
19 18 7 ringidcl โŠข ( ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring โ†’ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
20 15 19 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
21 18 8 grpinvcl โŠข ( ( ( Scalar โ€˜ ๐‘Š ) โˆˆ Grp โˆง ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โ†’ ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
22 17 20 21 syl2anc โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
23 simp3 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ๐‘‹ โˆˆ ๐‘ˆ )
24 5 6 18 1 lssvscl โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘‹ โˆˆ ๐‘ˆ ) ) โ†’ ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‹ ) โˆˆ ๐‘ˆ )
25 12 13 22 23 24 syl22anc โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‹ ) โˆˆ ๐‘ˆ )
26 11 25 eqeltrrd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘ โ€˜ ๐‘‹ ) โˆˆ ๐‘ˆ )