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

Metamath Proof Explorer

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	$⊢ \underset{˙}{+} = +_{W}$
		lssvancl.s	$⊢ S = LSubSp (W)$
		lssvancl.w	$⊢ φ \to W \in LMod$
		lssvancl.u	$⊢ φ \to U \in S$
		lssvancl.x	$⊢ φ \to X \in U$
		lssvancl.y	$⊢ φ \to Y \in V$
		lssvancl.n	$⊢ φ \to \neg Y \in U$
	Assertion	lssvancl2	$⊢ φ \to \neg Y \underset{˙}{+} X \in U$

Proof

Step	Hyp	Ref	Expression
1		lssvancl.v	$⊢ V = {Base}_{W}$
2		lssvancl.p	$⊢ \underset{˙}{+} = +_{W}$
3		lssvancl.s	$⊢ S = LSubSp (W)$
4		lssvancl.w	$⊢ φ \to W \in LMod$
5		lssvancl.u	$⊢ φ \to U \in S$
6		lssvancl.x	$⊢ φ \to X \in U$
7		lssvancl.y	$⊢ φ \to Y \in V$
8		lssvancl.n	$⊢ φ \to \neg Y \in U$
9	1 3	lssel	$⊢ (U \in S \land X \in U) \to X \in V$
10	5 6 9	syl2anc	$⊢ φ \to X \in V$
11	1 2	lmodcom	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
12	4 10 7 11	syl3anc	$⊢ φ \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
13	1 2 3 4 5 6 7 8	lssvancl1	$⊢ φ \to \neg X \underset{˙}{+} Y \in U$
14	12 13	eqneltrrd	$⊢ φ \to \neg Y \underset{˙}{+} X \in U$