Metamath Proof Explorer

Theorem lspsntrim

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

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

Proof

Step	Hyp	Ref	Expression
1		lspsntrim.v	$⊢ V = {Base}_{W}$
2		lspsntrim.s	$⊢ \underset{˙}{-} = -_{W}$
3		lspsntrim.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		lspsntrim.n	$⊢ N = LSpan (W)$
5		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
6	1 5	lmodvnegcl	$⊢ (W \in LMod \land Y \in V) \to {inv}_{g} (W) (Y) \in V$
7	6	3adant2	$⊢ (W \in LMod \land X \in V \land Y \in V) \to {inv}_{g} (W) (Y) \in V$
8		eqid	$⊢ +_{W} = +_{W}$
9	1 8 4 3	lspsntri	$⊢ (W \in LMod \land X \in V \land {inv}_{g} (W) (Y) \in V) \to N (\{X +_{W} {inv}_{g} (W) (Y)\}) \subseteq N (\{X\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Y)\})$
10	7 9	syld3an3	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X +_{W} {inv}_{g} (W) (Y)\}) \subseteq N (\{X\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Y)\})$
11	1 8 5 2	grpsubval	$⊢ (X \in V \land Y \in V) \to X \underset{˙}{-} Y = X +_{W} {inv}_{g} (W) (Y)$
12	11	sneqd	$⊢ (X \in V \land Y \in V) \to \{X \underset{˙}{-} Y\} = \{X +_{W} {inv}_{g} (W) (Y)\}$
13	12	fveq2d	$⊢ (X \in V \land Y \in V) \to N (\{X \underset{˙}{-} Y\}) = N (\{X +_{W} {inv}_{g} (W) (Y)\})$
14	13	3adant1	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{-} Y\}) = N (\{X +_{W} {inv}_{g} (W) (Y)\})$
15	1 5 4	lspsnneg	$⊢ (W \in LMod \land Y \in V) \to N (\{{inv}_{g} (W) (Y)\}) = N (\{Y\})$
16	15	3adant2	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{{inv}_{g} (W) (Y)\}) = N (\{Y\})$
17	16	eqcomd	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{Y\}) = N (\{{inv}_{g} (W) (Y)\})$
18	17	oveq2d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Y)\})$
19	10 14 18	3sstr4d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{-} Y\}) \subseteq N (\{X\}) \underset{˙}{\oplus} N (\{Y\})$