Theorem lssvancl2

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. (Contributed by NM, 20-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	lssvancl2	|- ( ph -> -. ( Y .+ X ) 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	1 3	lssel	|- ( ( U e. S /\ X e. U ) -> X e. V )
10	5 6 9	syl2anc	|- ( ph -> X e. V )
11	1 2	lmodcom	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) = ( Y .+ X ) )
12	4 10 7 11	syl3anc	|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )
13	1 2 3 4 5 6 7 8	lssvancl1	|- ( ph -> -. ( X .+ Y ) e. U )
14	12 13	eqneltrrd	|- ( ph -> -. ( Y .+ X ) e. U )