Metamath Proof Explorer

Theorem lssvsubcl

Description: Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lssvsubcl.m 
|- .- = ( -g ` W )
lssvsubcl.s 
|- S = ( LSubSp ` W )
Assertion lssvsubcl 
|- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .- Y ) e. U )

Proof

Step Hyp Ref Expression
1 lssvsubcl.m 
 |-  .- = ( -g ` W )
2 lssvsubcl.s 
 |-  S = ( LSubSp ` W )
3 simpll 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> W e. LMod )
4 eqid 
 |-  ( Base ` W ) = ( Base ` W )
5 4 2 lssel 
 |-  ( ( U e. S /\ X e. U ) -> X e. ( Base ` W ) )
6 5 ad2ant2lr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> X e. ( Base ` W ) )
7 4 2 lssel 
 |-  ( ( U e. S /\ Y e. U ) -> Y e. ( Base ` W ) )
8 7 ad2ant2l 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> Y e. ( Base ` W ) )
9 eqid 
 |-  ( +g ` W ) = ( +g ` W )
10 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
11 eqid 
 |-  ( .s ` W ) = ( .s ` W )
12 eqid 
 |-  ( invg ` ( Scalar ` W ) ) = ( invg ` ( Scalar ` W ) )
13 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
14 4 9 1 10 11 12 13 lmodvsubval2 
 |-  ( ( W e. LMod /\ X e. ( Base ` W ) /\ Y e. ( Base ` W ) ) -> ( X .- Y ) = ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ) )
15 3 6 8 14 syl3anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .- Y ) = ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ) )
16 10 lmodfgrp 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Grp )
17 3 16 syl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( Scalar ` W ) e. Grp )
18 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
19 10 18 13 lmod1cl 
 |-  ( W e. LMod -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
20 3 19 syl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
21 18 12 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 /\ Y e. U ) ) -> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) )
23 4 10 11 18 lmodvscl 
 |-  ( ( W e. LMod /\ ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) /\ Y e. ( Base ` W ) ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) e. ( Base ` W ) )
24 3 22 8 23 syl3anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) e. ( Base ` W ) )
25 4 9 lmodcom 
 |-  ( ( W e. LMod /\ X e. ( Base ` W ) /\ ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) e. ( Base ` W ) ) -> ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ) = ( ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ( +g ` W ) X ) )
26 3 6 24 25 syl3anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ) = ( ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ( +g ` W ) X ) )
27 simplr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> U e. S )
28 simprr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> Y e. U )
29 simprl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> X e. U )
30 10 18 9 11 2 lsscl 
 |-  ( ( U e. S /\ ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) /\ Y e. U /\ X e. U ) ) -> ( ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ( +g ` W ) X ) e. U )
31 27 22 28 29 30 syl13anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ( +g ` W ) X ) e. U )
32 26 31 eqeltrd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) Y ) ) e. U )
33 15 32 eqeltrd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .- Y ) e. U )