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 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) )
15 5 lmodring โŠข ( ๐‘Š โˆˆ LMod โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring )
16 15 3ad2ant1 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring )
17 16 ringgrpd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Grp )
18 14 7 ringidcl โŠข ( ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring โ†’ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
19 16 18 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
20 14 8 17 19 grpinvcld โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
21 simp3 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ๐‘‹ โˆˆ ๐‘ˆ )
22 5 6 14 1 lssvscl โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘‹ โˆˆ ๐‘ˆ ) ) โ†’ ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‹ ) โˆˆ ๐‘ˆ )
23 12 13 20 21 22 syl22anc โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( ( invg โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โ€˜ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‹ ) โˆˆ ๐‘ˆ )
24 11 23 eqeltrrd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘ โ€˜ ๐‘‹ ) โˆˆ ๐‘ˆ )