lsppr

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

Proof

Step	Hyp	Ref	Expression
1		lsppr.v	$⊢ V = {Base}_{W}$
2		lsppr.a	$⊢ \underset{˙}{+} = +_{W}$
3		lsppr.f	$⊢ F = Scalar (W)$
4		lsppr.k	$⊢ K = {Base}_{F}$
5		lsppr.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		lsppr.n	$⊢ N = LSpan (W)$
7		lsppr.w	$⊢ φ \to W \in LMod$
8		lsppr.x	$⊢ φ \to X \in V$
9		lsppr.y	$⊢ φ \to Y \in V$
10		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
11	10	fveq2i	$⊢ N (\{X, Y\}) = N (\{X\} \cup \{Y\})$
12	8	snssd	$⊢ φ \to \{X\} \subseteq V$
13	9	snssd	$⊢ φ \to \{Y\} \subseteq V$
14	1 6	lspun	$⊢ (W \in LMod \land \{X\} \subseteq V \land \{Y\} \subseteq V) \to N (\{X\} \cup \{Y\}) = N (N (\{X\}) \cup N (\{Y\}))$
15	7 12 13 14	syl3anc	$⊢ φ \to N (\{X\} \cup \{Y\}) = N (N (\{X\}) \cup N (\{Y\}))$
16		eqid	$⊢ LSubSp (W) = LSubSp (W)$
17	1 16 6	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
18	7 8 17	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (W)$
19	1 16 6	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
20	7 9 19	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
21		eqid	$⊢ LSSum (W) = LSSum (W)$
22	16 6 21	lsmsp	$⊢ (W \in LMod \land N (\{X\}) \in LSubSp (W) \land N (\{Y\}) \in LSubSp (W)) \to N (\{X\}) LSSum (W) N (\{Y\}) = N (N (\{X\}) \cup N (\{Y\}))$
23	7 18 20 22	syl3anc	$⊢ φ \to N (\{X\}) LSSum (W) N (\{Y\}) = N (N (\{X\}) \cup N (\{Y\}))$
24	1 2 3 4 5 21 6 7 8 9	lsmspsn	$⊢ φ \to (v \in (N (\{X\}) LSSum (W) N (\{Y\})) \leftrightarrow \exists k \in K \exists l \in K v = (k \underset{˙}{\cdot} X) \underset{˙}{+} (l \underset{˙}{\cdot} Y))$
25	24	abbi2dv	$⊢ φ \to N (\{X\}) LSSum (W) N (\{Y\}) = \{v \| \exists k \in K \exists l \in K v = (k \underset{˙}{\cdot} X) \underset{˙}{+} (l \underset{˙}{\cdot} Y)\}$
26	15 23 25	3eqtr2d	$⊢ φ \to N (\{X\} \cup \{Y\}) = \{v \| \exists k \in K \exists l \in K v = (k \underset{˙}{\cdot} X) \underset{˙}{+} (l \underset{˙}{\cdot} Y)\}$
27	11 26	eqtrid	$⊢ φ \to N (\{X, Y\}) = \{v \| \exists k \in K \exists l \in K v = (k \underset{˙}{\cdot} X) \underset{˙}{+} (l \underset{˙}{\cdot} Y)\}$

Metamath Proof Explorer

Theorem lsppr

Proof