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={\mathrm{Base}}_W$$
	lssvancl.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lssvancl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lssvancl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lssvancl.u	$$⊢\phi \to U\in S$$
	lssvancl.x	$$⊢\phi \to X\in U$$
	lssvancl.y	$$⊢\phi \to Y\in V$$
	lssvancl.n	$$⊢\phi \to \neg Y\in U$$
Assertion	lssvancl1	$$⊢\phi \to \neg X\underset{\dot{}}{+}Y\in U$$

Proof

Step	Hyp	Ref	Expression
1		lssvancl.v	$$⊢V={\mathrm{Base}}_W$$
2		lssvancl.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lssvancl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
4		lssvancl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lssvancl.u	$$⊢\phi \to U\in S$$
6		lssvancl.x	$$⊢\phi \to X\in U$$
7		lssvancl.y	$$⊢\phi \to Y\in V$$
8		lssvancl.n	$$⊢\phi \to \neg Y\in U$$
9		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
10	4 9	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
11	1 3	lssel	$$⊢\left(U\in S\wedge X\in U\right)\to X\in V$$
12	5 6 11	syl2anc	$$⊢\phi \to X\in V$$
13		eqid	$$⊢{-}_W={-}_W$$
14	1 2 13	ablpncan2	$$⊢\left(W\in \mathrm{Abel}\wedge X\in V\wedge Y\in V\right)\to \left(X\underset{\dot{}}{+}Y\right){-}_{W}X=Y$$
15	10 12 7 14	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right){-}_{W}X=Y$$
16	15	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in U\right)\to \left(X\underset{\dot{}}{+}Y\right){-}_{W}X=Y$$
17	4	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in U\right)\to W\in \mathrm{LMod}$$
18	5	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in U\right)\to U\in S$$
19		simpr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in U\right)\to X\underset{\dot{}}{+}Y\in U$$
20	6	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in U\right)\to X\in U$$
21	13 3	lssvsubcl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge U\in S\right)\wedge \left(X\underset{\dot{}}{+}Y\in U\wedge X\in U\right)\right)\to \left(X\underset{\dot{}}{+}Y\right){-}_{W}X\in U$$
22	17 18 19 20 21	syl22anc	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in U\right)\to \left(X\underset{\dot{}}{+}Y\right){-}_{W}X\in U$$
23	16 22	eqeltrrd	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in U\right)\to Y\in U$$
24	8 23	mtand	$$⊢\phi \to \neg X\underset{\dot{}}{+}Y\in U$$