lspprvacl

Description: The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015)

Step	Hyp	Ref	Expression
1		lspprvacl.v	$⊢ V = {Base}_{W}$
2		lspprvacl.p	$⊢ \underset{˙}{+} = +_{W}$
3		lspprvacl.n	$⊢ N = LSpan (W)$
4		lspprvacl.w	$⊢ φ \to W \in LMod$
5		lspprvacl.x	$⊢ φ \to X \in V$
6		lspprvacl.y	$⊢ φ \to Y \in V$
7		eqid	$⊢ LSubSp (W) = LSubSp (W)$
8	1 7 3 4 5 6	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (W)$
9	1 3 4 5 6	lspprid1	$⊢ φ \to X \in N (\{X, Y\})$
10	1 3 4 5 6	lspprid2	$⊢ φ \to Y \in N (\{X, Y\})$
11	2 7	lssvacl	$⊢ ((W \in LMod \land N (\{X, Y\}) \in LSubSp (W)) \land (X \in N (\{X, Y\}) \land Y \in N (\{X, Y\}))) \to X \underset{˙}{+} Y \in N (\{X, Y\})$
12	4 8 9 10 11	syl22anc	$⊢ φ \to X \underset{˙}{+} Y \in N (\{X, Y\})$

Metamath Proof Explorer