Metamath Proof Explorer

Theorem lspvadd

Description: The span of a vector sum is included in the span of its arguments. (Contributed by NM, 22-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

		Ref	Expression
	Hypotheses	lspvadd.v	$⊢ V = {Base}_{W}$
		lspvadd.a	$⊢ \underset{˙}{+} = +_{W}$
		lspvadd.n	$⊢ N = LSpan (W)$
	Assertion	lspvadd	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X, Y\})$

Proof

Step	Hyp	Ref	Expression
1		lspvadd.v	$⊢ V = {Base}_{W}$
2		lspvadd.a	$⊢ \underset{˙}{+} = +_{W}$
3		lspvadd.n	$⊢ N = LSpan (W)$
4		eqid	$⊢ LSubSp (W) = LSubSp (W)$
5		simp1	$⊢ (W \in LMod \land X \in V \land Y \in V) \to W \in LMod$
6		prssi	$⊢ (X \in V \land Y \in V) \to \{X, Y\} \subseteq V$
7	6	3adant1	$⊢ (W \in LMod \land X \in V \land Y \in V) \to \{X, Y\} \subseteq V$
8	1 4 3	lspcl	$⊢ (W \in LMod \land \{X, Y\} \subseteq V) \to N (\{X, Y\}) \in LSubSp (W)$
9	5 7 8	syl2anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X, Y\}) \in LSubSp (W)$
10	1 3	lspssid	$⊢ (W \in LMod \land \{X, Y\} \subseteq V) \to \{X, Y\} \subseteq N (\{X, Y\})$
11	5 7 10	syl2anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to \{X, Y\} \subseteq N (\{X, Y\})$
12		prssg	$⊢ (X \in V \land Y \in V) \to ((X \in N (\{X, Y\}) \land Y \in N (\{X, Y\})) \leftrightarrow \{X, Y\} \subseteq N (\{X, Y\}))$
13	12	3adant1	$⊢ (W \in LMod \land X \in V \land Y \in V) \to ((X \in N (\{X, Y\}) \land Y \in N (\{X, Y\})) \leftrightarrow \{X, Y\} \subseteq N (\{X, Y\}))$
14	11 13	mpbird	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \in N (\{X, Y\}) \land Y \in N (\{X, Y\}))$
15	2 4	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\})$
16	5 9 14 15	syl21anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y \in N (\{X, Y\})$
17	4 3 5 9 16	lspsnel5a	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X, Y\})$