lspsntri

Description: Triangle-type inequality for span of a singleton. (Contributed by NM, 24-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014)

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

Step	Hyp	Ref	Expression
1		lspsntri.v	$⊢ V = {Base}_{W}$
2		lspsntri.a	$⊢ \underset{˙}{+} = +_{W}$
3		lspsntri.n	$⊢ N = LSpan (W)$
4		lspsntri.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5	1 2 3	lspvadd	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X, Y\})$
6		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
7	6	fveq2i	$⊢ N (\{X, Y\}) = N (\{X\} \cup \{Y\})$
8	5 7	sseqtrdi	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\} \cup \{Y\})$
9		simp1	$⊢ (W \in LMod \land X \in V \land Y \in V) \to W \in LMod$
10		simp2	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \in V$
11	10	snssd	$⊢ (W \in LMod \land X \in V \land Y \in V) \to \{X\} \subseteq V$
12		simp3	$⊢ (W \in LMod \land X \in V \land Y \in V) \to Y \in V$
13	12	snssd	$⊢ (W \in LMod \land X \in V \land Y \in V) \to \{Y\} \subseteq V$
14	1 3 4	lsmsp2	$⊢ (W \in LMod \land \{X\} \subseteq V \land \{Y\} \subseteq V) \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\} \cup \{Y\})$
15	9 11 13 14	syl3anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\} \cup \{Y\})$
16	8 15	sseqtrrd	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) \underset{˙}{\oplus} N (\{Y\})$

Metamath Proof Explorer