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 )