lsmcl

Description: The sum of two subspaces is a subspace. (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		lsmcl.s	$⊢ S = LSubSp (W)$
2		lsmcl.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lmodabl	$⊢ W \in LMod \to W \in Abel$
4	3	3ad2ant1	$⊢ (W \in LMod \land T \in S \land U \in S) \to W \in Abel$
5	1	lsssubg	$⊢ (W \in LMod \land T \in S) \to T \in SubGrp (W)$
6	5	3adant3	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \in SubGrp (W)$
7	1	lsssubg	$⊢ (W \in LMod \land U \in S) \to U \in SubGrp (W)$
8	7	3adant2	$⊢ (W \in LMod \land T \in S \land U \in S) \to U \in SubGrp (W)$
9	2	lsmsubg2	$⊢ (W \in Abel \land T \in SubGrp (W) \land U \in SubGrp (W)) \to T \underset{˙}{\oplus} U \in SubGrp (W)$
10	4 6 8 9	syl3anc	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \underset{˙}{\oplus} U \in SubGrp (W)$
11		eqid	$⊢ +_{W} = +_{W}$
12	11 2	lsmelval	$⊢ (T \in SubGrp (W) \land U \in SubGrp (W)) \to (u \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists d \in T \exists e \in U u = d +_{W} e)$
13	6 8 12	syl2anc	$⊢ (W \in LMod \land T \in S \land U \in S) \to (u \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists d \in T \exists e \in U u = d +_{W} e)$
14	13	adantr	$⊢ ((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \to (u \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists d \in T \exists e \in U u = d +_{W} e)$
15		simpll1	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to W \in LMod$
16		simplr	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to a \in {Base}_{Scalar (W)}$
17		simpll2	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to T \in S$
18		simprl	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to d \in T$
19		eqid	$⊢ {Base}_{W} = {Base}_{W}$
20	19 1	lssel	$⊢ (T \in S \land d \in T) \to d \in {Base}_{W}$
21	17 18 20	syl2anc	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to d \in {Base}_{W}$
22		simpll3	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to U \in S$
23		simprr	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to e \in U$
24	19 1	lssel	$⊢ (U \in S \land e \in U) \to e \in {Base}_{W}$
25	22 23 24	syl2anc	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to e \in {Base}_{W}$
26		eqid	$⊢ Scalar (W) = Scalar (W)$
27		eqid	$⊢ \cdot_{W} = \cdot_{W}$
28		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
29	19 11 26 27 28	lmodvsdi	$⊢ (W \in LMod \land (a \in {Base}_{Scalar (W)} \land d \in {Base}_{W} \land e \in {Base}_{W})) \to a \cdot_{W} (d +_{W} e) = (a \cdot_{W} d) +_{W} (a \cdot_{W} e)$
30	15 16 21 25 29	syl13anc	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to a \cdot_{W} (d +_{W} e) = (a \cdot_{W} d) +_{W} (a \cdot_{W} e)$
31	15 17 5	syl2anc	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to T \in SubGrp (W)$
32	15 22 7	syl2anc	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to U \in SubGrp (W)$
33	26 27 28 1	lssvscl	$⊢ ((W \in LMod \land T \in S) \land (a \in {Base}_{Scalar (W)} \land d \in T)) \to a \cdot_{W} d \in T$
34	15 17 16 18 33	syl22anc	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to a \cdot_{W} d \in T$
35	26 27 28 1	lssvscl	$⊢ ((W \in LMod \land U \in S) \land (a \in {Base}_{Scalar (W)} \land e \in U)) \to a \cdot_{W} e \in U$
36	15 22 16 23 35	syl22anc	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to a \cdot_{W} e \in U$
37	11 2	lsmelvali	$⊢ ((T \in SubGrp (W) \land U \in SubGrp (W)) \land (a \cdot_{W} d \in T \land a \cdot_{W} e \in U)) \to (a \cdot_{W} d) +_{W} (a \cdot_{W} e) \in (T \underset{˙}{\oplus} U)$
38	31 32 34 36 37	syl22anc	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to (a \cdot_{W} d) +_{W} (a \cdot_{W} e) \in (T \underset{˙}{\oplus} U)$
39	30 38	eqeltrd	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to a \cdot_{W} (d +_{W} e) \in (T \underset{˙}{\oplus} U)$
40		oveq2	$⊢ u = d +_{W} e \to a \cdot_{W} u = a \cdot_{W} (d +_{W} e)$
41	40	eleq1d	$⊢ u = d +_{W} e \to (a \cdot_{W} u \in (T \underset{˙}{\oplus} U) \leftrightarrow a \cdot_{W} (d +_{W} e) \in (T \underset{˙}{\oplus} U))$
42	39 41	syl5ibrcom	$⊢ (((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \land (d \in T \land e \in U)) \to (u = d +_{W} e \to a \cdot_{W} u \in (T \underset{˙}{\oplus} U))$
43	42	rexlimdvva	$⊢ ((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \to (\exists d \in T \exists e \in U u = d +_{W} e \to a \cdot_{W} u \in (T \underset{˙}{\oplus} U))$
44	14 43	sylbid	$⊢ ((W \in LMod \land T \in S \land U \in S) \land a \in {Base}_{Scalar (W)}) \to (u \in (T \underset{˙}{\oplus} U) \to a \cdot_{W} u \in (T \underset{˙}{\oplus} U))$
45	44	impr	$⊢ ((W \in LMod \land T \in S \land U \in S) \land (a \in {Base}_{Scalar (W)} \land u \in (T \underset{˙}{\oplus} U))) \to a \cdot_{W} u \in (T \underset{˙}{\oplus} U)$
46	45	ralrimivva	$⊢ (W \in LMod \land T \in S \land U \in S) \to \forall a \in {Base}_{Scalar (W)} \forall u \in (T \underset{˙}{\oplus} U) a \cdot_{W} u \in (T \underset{˙}{\oplus} U)$
47	26 28 19 27 1	islss4	$⊢ W \in LMod \to (T \underset{˙}{\oplus} U \in S \leftrightarrow (T \underset{˙}{\oplus} U \in SubGrp (W) \land \forall a \in {Base}_{Scalar (W)} \forall u \in (T \underset{˙}{\oplus} U) a \cdot_{W} u \in (T \underset{˙}{\oplus} U)))$
48	47	3ad2ant1	$⊢ (W \in LMod \land T \in S \land U \in S) \to (T \underset{˙}{\oplus} U \in S \leftrightarrow (T \underset{˙}{\oplus} U \in SubGrp (W) \land \forall a \in {Base}_{Scalar (W)} \forall u \in (T \underset{˙}{\oplus} U) a \cdot_{W} u \in (T \underset{˙}{\oplus} U)))$
49	10 46 48	mpbir2and	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \underset{˙}{\oplus} U \in S$

Metamath Proof Explorer

Theorem lsmcl

Proof