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 = ( LSubSp ` W )
lssvnegcl.n 
|- N = ( invg ` W )
Assertion lssvnegcl 
|- ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` X ) e. U )

Proof

Step Hyp Ref Expression
1 lssvnegcl.s 
 |-  S = ( LSubSp ` W )
2 lssvnegcl.n 
 |-  N = ( invg ` W )
3 eqid 
 |-  ( Base ` W ) = ( Base ` W )
4 3 1 lssel 
 |-  ( ( U e. S /\ X e. U ) -> X e. ( Base ` W ) )
5 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 eqid 
 |-  ( .s ` W ) = ( .s ` W )
7 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
8 eqid 
 |-  ( invg ` ( Scalar ` W ) ) = ( invg ` ( Scalar ` W ) )
9 3 2 5 6 7 8 lmodvneg1 
 |-  ( ( W e. LMod /\ X e. ( Base ` W ) ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) X ) = ( N ` X ) )
10 4 9 sylan2 
 |-  ( ( W e. LMod /\ ( U e. S /\ X e. U ) ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) X ) = ( N ` X ) )
11 10 3impb 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) X ) = ( N ` X ) )
12 simp1 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> W e. LMod )
13 simp2 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> U e. S )
14 5 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
15 14 3ad2ant1 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( Scalar ` W ) e. Ring )
16 ringgrp 
 |-  ( ( Scalar ` W ) e. Ring -> ( Scalar ` W ) e. Grp )
17 15 16 syl 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( Scalar ` W ) e. Grp )
18 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
19 18 7 ringidcl 
 |-  ( ( Scalar ` W ) e. Ring -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
20 15 19 syl 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
21 18 8 grpinvcl 
 |-  ( ( ( Scalar ` W ) e. Grp /\ ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) )
22 17 20 21 syl2anc 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) )
23 simp3 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> X e. U )
24 5 6 18 1 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) /\ X e. U ) ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) X ) e. U )
25 12 13 22 23 24 syl22anc 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) X ) e. U )
26 11 25 eqeltrrd 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` X ) e. U )