lsppreli

Description: A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015)

	Ref	Expression
Hypotheses	lsppreli.v	$⊢ V = {Base}_{W}$
	lsppreli.p	$⊢ \underset{˙}{+} = +_{W}$
	lsppreli.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lsppreli.f	$⊢ F = Scalar (W)$
	lsppreli.k	$⊢ K = {Base}_{F}$
	lsppreli.n	$⊢ N = LSpan (W)$
	lsppreli.w	$⊢ φ \to W \in LMod$
	lsppreli.a	$⊢ φ \to A \in K$
	lsppreli.b	$⊢ φ \to B \in K$
	lsppreli.x	$⊢ φ \to X \in V$
	lsppreli.y	$⊢ φ \to Y \in V$
Assertion	lsppreli	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y) \in N (\{X, Y\})$

Step	Hyp	Ref	Expression
1		lsppreli.v	$⊢ V = {Base}_{W}$
2		lsppreli.p	$⊢ \underset{˙}{+} = +_{W}$
3		lsppreli.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lsppreli.f	$⊢ F = Scalar (W)$
5		lsppreli.k	$⊢ K = {Base}_{F}$
6		lsppreli.n	$⊢ N = LSpan (W)$
7		lsppreli.w	$⊢ φ \to W \in LMod$
8		lsppreli.a	$⊢ φ \to A \in K$
9		lsppreli.b	$⊢ φ \to B \in K$
10		lsppreli.x	$⊢ φ \to X \in V$
11		lsppreli.y	$⊢ φ \to Y \in V$
12	1 6	lspsnsubg	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in SubGrp (W)$
13	7 10 12	syl2anc	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
14	1 6	lspsnsubg	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in SubGrp (W)$
15	7 11 14	syl2anc	$⊢ φ \to N (\{Y\}) \in SubGrp (W)$
16	1 3 4 5 6 7 8 10	ellspsni	$⊢ φ \to A \underset{˙}{\cdot} X \in N (\{X\})$
17	1 3 4 5 6 7 9 11	ellspsni	$⊢ φ \to B \underset{˙}{\cdot} Y \in N (\{Y\})$
18		eqid	$⊢ LSSum (W) = LSSum (W)$
19	2 18	lsmelvali	$⊢ ((N (\{X\}) \in SubGrp (W) \land N (\{Y\}) \in SubGrp (W)) \land (A \underset{˙}{\cdot} X \in N (\{X\}) \land B \underset{˙}{\cdot} Y \in N (\{Y\}))) \to (A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y) \in (N (\{X\}) LSSum (W) N (\{Y\}))$
20	13 15 16 17 19	syl22anc	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y) \in (N (\{X\}) LSSum (W) N (\{Y\}))$
21	1 6 18 7 10 11	lsmpr	$⊢ φ \to N (\{X, Y\}) = N (\{X\}) LSSum (W) N (\{Y\})$
22	20 21	eleqtrrd	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y) \in N (\{X, Y\})$

Metamath Proof Explorer