lsmssspx

Description: Subspace sum (in its extended domain) is a subset of the span of the union of its arguments. (Contributed by NM, 6-Aug-2014)

	Ref	Expression
Hypotheses	lsmsp2.v	$⊢ V = {Base}_{W}$
	lsmsp2.n	$⊢ N = LSpan (W)$
	lsmsp2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmssspx.t	$⊢ φ \to T \subseteq V$
	lsmssspx.u	$⊢ φ \to U \subseteq V$
	lsmssspx.w	$⊢ φ \to W \in LMod$
Assertion	lsmssspx	$⊢ φ \to T \underset{˙}{\oplus} U \subseteq 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		lsmssspx.t	$⊢ φ \to T \subseteq V$
5		lsmssspx.u	$⊢ φ \to U \subseteq V$
6		lsmssspx.w	$⊢ φ \to W \in LMod$
7	1 2	lspssv	$⊢ (W \in LMod \land T \subseteq V) \to N (T) \subseteq V$
8	6 4 7	syl2anc	$⊢ φ \to N (T) \subseteq V$
9	1 2	lspssid	$⊢ (W \in LMod \land T \subseteq V) \to T \subseteq N (T)$
10	6 4 9	syl2anc	$⊢ φ \to T \subseteq N (T)$
11	1 3	lsmless1x	$⊢ ((W \in LMod \land N (T) \subseteq V \land U \subseteq V) \land T \subseteq N (T)) \to T \underset{˙}{\oplus} U \subseteq N (T) \underset{˙}{\oplus} U$
12	6 8 5 10 11	syl31anc	$⊢ φ \to T \underset{˙}{\oplus} U \subseteq N (T) \underset{˙}{\oplus} U$
13	1 2	lspssv	$⊢ (W \in LMod \land U \subseteq V) \to N (U) \subseteq V$
14	6 5 13	syl2anc	$⊢ φ \to N (U) \subseteq V$
15	1 2	lspssid	$⊢ (W \in LMod \land U \subseteq V) \to U \subseteq N (U)$
16	6 5 15	syl2anc	$⊢ φ \to U \subseteq N (U)$
17	1 3	lsmless2x	$⊢ ((W \in LMod \land N (T) \subseteq V \land N (U) \subseteq V) \land U \subseteq N (U)) \to N (T) \underset{˙}{\oplus} U \subseteq N (T) \underset{˙}{\oplus} N (U)$
18	6 8 14 16 17	syl31anc	$⊢ φ \to N (T) \underset{˙}{\oplus} U \subseteq N (T) \underset{˙}{\oplus} N (U)$
19	12 18	sstrd	$⊢ φ \to T \underset{˙}{\oplus} U \subseteq N (T) \underset{˙}{\oplus} N (U)$
20	1 2 3	lsmsp2	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T) \underset{˙}{\oplus} N (U) = N (T \cup U)$
21	6 4 5 20	syl3anc	$⊢ φ \to N (T) \underset{˙}{\oplus} N (U) = N (T \cup U)$
22	19 21	sseqtrd	$⊢ φ \to T \underset{˙}{\oplus} U \subseteq N (T \cup U)$

Metamath Proof Explorer

Theorem lsmssspx

Proof