Metamath Proof Explorer

Theorem lsmsp2

Description: Subspace sum of spans of subsets is the span of their union. ( spanuni analog.) (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014)

		Ref	Expression
	Hypotheses	lsmsp2.v	$⊢ V = {Base}_{W}$
		lsmsp2.n	$⊢ N = LSpan (W)$
		lsmsp2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	Assertion	lsmsp2	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T) \underset{˙}{\oplus} N (U) = N (T \cup U)$

Proof

Step	Hyp	Ref	Expression
1		lsmsp2.v	$⊢ V = {Base}_{W}$
2		lsmsp2.n	$⊢ N = LSpan (W)$
3		lsmsp2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		simp1	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to W \in LMod$
5		eqid	$⊢ LSubSp (W) = LSubSp (W)$
6	1 5 2	lspcl	$⊢ (W \in LMod \land T \subseteq V) \to N (T) \in LSubSp (W)$
7	6	3adant3	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T) \in LSubSp (W)$
8	1 5 2	lspcl	$⊢ (W \in LMod \land U \subseteq V) \to N (U) \in LSubSp (W)$
9	8	3adant2	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (U) \in LSubSp (W)$
10	5 2 3	lsmsp	$⊢ (W \in LMod \land N (T) \in LSubSp (W) \land N (U) \in LSubSp (W)) \to N (T) \underset{˙}{\oplus} N (U) = N (N (T) \cup N (U))$
11	4 7 9 10	syl3anc	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T) \underset{˙}{\oplus} N (U) = N (N (T) \cup N (U))$
12	1 2	lspun	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T \cup U) = N (N (T) \cup N (U))$
13	11 12	eqtr4d	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T) \underset{˙}{\oplus} N (U) = N (T \cup U)$