lsmpr

Description: The span of a pair of vectors equals the sum of the spans of their singletons. (Contributed by NM, 13-Jan-2015)

Step	Hyp	Ref	Expression
1		lsmpr.v	$⊢ V = {Base}_{W}$
2		lsmpr.n	$⊢ N = LSpan (W)$
3		lsmpr.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		lsmpr.w	$⊢ φ \to W \in LMod$
5		lsmpr.x	$⊢ φ \to X \in V$
6		lsmpr.y	$⊢ φ \to Y \in V$
7	5	snssd	$⊢ φ \to \{X\} \subseteq V$
8	6	snssd	$⊢ φ \to \{Y\} \subseteq V$
9	1 2	lspun	$⊢ (W \in LMod \land \{X\} \subseteq V \land \{Y\} \subseteq V) \to N (\{X\} \cup \{Y\}) = N (N (\{X\}) \cup N (\{Y\}))$
10	4 7 8 9	syl3anc	$⊢ φ \to N (\{X\} \cup \{Y\}) = N (N (\{X\}) \cup N (\{Y\}))$
11		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
12	11	fveq2i	$⊢ N (\{X, Y\}) = N (\{X\} \cup \{Y\})$
13	12	a1i	$⊢ φ \to N (\{X, Y\}) = N (\{X\} \cup \{Y\})$
14		eqid	$⊢ LSubSp (W) = LSubSp (W)$
15	1 14 2	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
16	4 5 15	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (W)$
17	1 14 2	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
18	4 6 17	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
19	14 2 3	lsmsp	$⊢ (W \in LMod \land N (\{X\}) \in LSubSp (W) \land N (\{Y\}) \in LSubSp (W)) \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (N (\{X\}) \cup N (\{Y\}))$
20	4 16 18 19	syl3anc	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (N (\{X\}) \cup N (\{Y\}))$
21	10 13 20	3eqtr4d	$⊢ φ \to N (\{X, Y\}) = N (\{X\}) \underset{˙}{\oplus} N (\{Y\})$

Metamath Proof Explorer