lsmsp

Description: Subspace sum in terms of span. (Contributed by NM, 6-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

	Ref	Expression
Hypotheses	lsmsp.s	$⊢ S = LSubSp (W)$
	lsmsp.n	$⊢ N = LSpan (W)$
	lsmsp.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
Assertion	lsmsp	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \underset{˙}{\oplus} U = N (T \cup U)$

Proof

Step	Hyp	Ref	Expression
1		lsmsp.s	$⊢ S = LSubSp (W)$
2		lsmsp.n	$⊢ N = LSpan (W)$
3		lsmsp.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		simp1	$⊢ (W \in LMod \land T \in S \land U \in S) \to W \in LMod$
5		eqid	$⊢ {Base}_{W} = {Base}_{W}$
6	5 1	lssss	$⊢ T \in S \to T \subseteq {Base}_{W}$
7	6	3ad2ant2	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \subseteq {Base}_{W}$
8	5 1	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
9	8	3ad2ant3	$⊢ (W \in LMod \land T \in S \land U \in S) \to U \subseteq {Base}_{W}$
10	7 9	unssd	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \cup U \subseteq {Base}_{W}$
11	5 2	lspssid	$⊢ (W \in LMod \land T \cup U \subseteq {Base}_{W}) \to T \cup U \subseteq N (T \cup U)$
12	4 10 11	syl2anc	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \cup U \subseteq N (T \cup U)$
13	12	unssad	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \subseteq N (T \cup U)$
14	12	unssbd	$⊢ (W \in LMod \land T \in S \land U \in S) \to U \subseteq N (T \cup U)$
15	1	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
16	15	3ad2ant1	$⊢ (W \in LMod \land T \in S \land U \in S) \to S \subseteq SubGrp (W)$
17		simp2	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \in S$
18	16 17	sseldd	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \in SubGrp (W)$
19		simp3	$⊢ (W \in LMod \land T \in S \land U \in S) \to U \in S$
20	16 19	sseldd	$⊢ (W \in LMod \land T \in S \land U \in S) \to U \in SubGrp (W)$
21	5 1 2	lspcl	$⊢ (W \in LMod \land T \cup U \subseteq {Base}_{W}) \to N (T \cup U) \in S$
22	4 10 21	syl2anc	$⊢ (W \in LMod \land T \in S \land U \in S) \to N (T \cup U) \in S$
23	16 22	sseldd	$⊢ (W \in LMod \land T \in S \land U \in S) \to N (T \cup U) \in SubGrp (W)$
24	3	lsmlub	$⊢ (T \in SubGrp (W) \land U \in SubGrp (W) \land N (T \cup U) \in SubGrp (W)) \to ((T \subseteq N (T \cup U) \land U \subseteq N (T \cup U)) \leftrightarrow T \underset{˙}{\oplus} U \subseteq N (T \cup U))$
25	18 20 23 24	syl3anc	$⊢ (W \in LMod \land T \in S \land U \in S) \to ((T \subseteq N (T \cup U) \land U \subseteq N (T \cup U)) \leftrightarrow T \underset{˙}{\oplus} U \subseteq N (T \cup U))$
26	13 14 25	mpbi2and	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \underset{˙}{\oplus} U \subseteq N (T \cup U)$
27	1 3	lsmcl	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \underset{˙}{\oplus} U \in S$
28	3	lsmunss	$⊢ (T \in SubGrp (W) \land U \in SubGrp (W)) \to T \cup U \subseteq T \underset{˙}{\oplus} U$
29	18 20 28	syl2anc	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \cup U \subseteq T \underset{˙}{\oplus} U$
30	1 2	lspssp	$⊢ (W \in LMod \land T \underset{˙}{\oplus} U \in S \land T \cup U \subseteq T \underset{˙}{\oplus} U) \to N (T \cup U) \subseteq T \underset{˙}{\oplus} U$
31	4 27 29 30	syl3anc	$⊢ (W \in LMod \land T \in S \land U \in S) \to N (T \cup U) \subseteq T \underset{˙}{\oplus} U$
32	26 31	eqssd	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \underset{˙}{\oplus} U = N (T \cup U)$

Metamath Proof Explorer

Theorem lsmsp

Proof