This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
15 5 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
16 15 3ad2ant1 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( Scalar ` W ) e. Ring )
17 16 ringgrpd 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( Scalar ` W ) e. Grp )
18 14 7 ringidcl 
 |-  ( ( Scalar ` W ) e. Ring -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
19 16 18 syl 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
20 14 8 17 19 grpinvcld 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) )
21 simp3 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> X e. U )
22 5 6 14 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 )
23 12 13 20 21 22 syl22anc 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) X ) e. U )
24 11 23 eqeltrrd 
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` X ) e. U )