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={\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	lssvancl2	$$⊢\phi \to \neg Y\underset{\dot{}}{+}X\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	1 3	lssel	$$⊢\left(U\in S\wedge X\in U\right)\to X\in V$$
10	5 6 9	syl2anc	$$⊢\phi \to X\in V$$
11	1 2	lmodcom	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
12	4 10 7 11	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
13	1 2 3 4 5 6 7 8	lssvancl1	$$⊢\phi \to \neg X\underset{\dot{}}{+}Y\in U$$
14	12 13	eqneltrrd	$$⊢\phi \to \neg Y\underset{\dot{}}{+}X\in U$$