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

Metamath Proof Explorer

Theorem lssvancl1

Description: Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. TODO: notice similarity to lspindp3 . Can it be used along with lspsnne1 , lspsnne2 to shorten this proof? (Contributed by NM, 14-May-2015)

Ref Expression
Hypotheses lssvancl.v 
|- V = ( Base ` W )
lssvancl.p 
|- .+ = ( +g ` W )
lssvancl.s 
|- S = ( LSubSp ` W )
lssvancl.w 
|- ( ph -> W e. LMod )
lssvancl.u 
|- ( ph -> U e. S )
lssvancl.x 
|- ( ph -> X e. U )
lssvancl.y 
|- ( ph -> Y e. V )
lssvancl.n 
|- ( ph -> -. Y e. U )
Assertion lssvancl1 
|- ( ph -> -. ( X .+ Y ) e. U )

Proof

Step Hyp Ref Expression
1 lssvancl.v 
 |-  V = ( Base ` W )
2 lssvancl.p 
 |-  .+ = ( +g ` W )
3 lssvancl.s 
 |-  S = ( LSubSp ` W )
4 lssvancl.w 
 |-  ( ph -> W e. LMod )
5 lssvancl.u 
 |-  ( ph -> U e. S )
6 lssvancl.x 
 |-  ( ph -> X e. U )
7 lssvancl.y 
 |-  ( ph -> Y e. V )
8 lssvancl.n 
 |-  ( ph -> -. Y e. U )
9 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
10 4 9 syl 
 |-  ( ph -> W e. Abel )
11 1 3 lssel 
 |-  ( ( U e. S /\ X e. U ) -> X e. V )
12 5 6 11 syl2anc 
 |-  ( ph -> X e. V )
13 eqid 
 |-  ( -g ` W ) = ( -g ` W )
14 1 2 13 ablpncan2 
 |-  ( ( W e. Abel /\ X e. V /\ Y e. V ) -> ( ( X .+ Y ) ( -g ` W ) X ) = Y )
15 10 12 7 14 syl3anc 
 |-  ( ph -> ( ( X .+ Y ) ( -g ` W ) X ) = Y )
16 15 adantr 
 |-  ( ( ph /\ ( X .+ Y ) e. U ) -> ( ( X .+ Y ) ( -g ` W ) X ) = Y )
17 4 adantr 
 |-  ( ( ph /\ ( X .+ Y ) e. U ) -> W e. LMod )
18 5 adantr 
 |-  ( ( ph /\ ( X .+ Y ) e. U ) -> U e. S )
19 simpr 
 |-  ( ( ph /\ ( X .+ Y ) e. U ) -> ( X .+ Y ) e. U )
20 6 adantr 
 |-  ( ( ph /\ ( X .+ Y ) e. U ) -> X e. U )
21 13 3 lssvsubcl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( ( X .+ Y ) e. U /\ X e. U ) ) -> ( ( X .+ Y ) ( -g ` W ) X ) e. U )
22 17 18 19 20 21 syl22anc 
 |-  ( ( ph /\ ( X .+ Y ) e. U ) -> ( ( X .+ Y ) ( -g ` W ) X ) e. U )
23 16 22 eqeltrrd 
 |-  ( ( ph /\ ( X .+ Y ) e. U ) -> Y e. U )
24 8 23 mtand 
 |-  ( ph -> -. ( X .+ Y ) e. U )