lssvacl

Description: Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lssvacl.p	$⊢ \underset{˙}{+} = +_{W}$
	lssvacl.s	$⊢ S = LSubSp (W)$
Assertion	lssvacl	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to X \underset{˙}{+} Y \in U$

Proof

Step	Hyp	Ref	Expression
1		lssvacl.p	$⊢ \underset{˙}{+} = +_{W}$
2		lssvacl.s	$⊢ S = LSubSp (W)$
3		simpll	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to W \in LMod$
4		eqid	$⊢ {Base}_{W} = {Base}_{W}$
5	4 2	lssel	$⊢ (U \in S \land X \in U) \to X \in {Base}_{W}$
6	5	ad2ant2lr	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to X \in {Base}_{W}$
7		eqid	$⊢ Scalar (W) = Scalar (W)$
8		eqid	$⊢ \cdot_{W} = \cdot_{W}$
9		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
10	4 7 8 9	lmodvs1	$⊢ (W \in LMod \land X \in {Base}_{W}) \to 1_{Scalar (W)} \cdot_{W} X = X$
11	3 6 10	syl2anc	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to 1_{Scalar (W)} \cdot_{W} X = X$
12	11	oveq1d	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to (1_{Scalar (W)} \cdot_{W} X) \underset{˙}{+} Y = X \underset{˙}{+} Y$
13		simplr	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to U \in S$
14		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
15	7 14 9	lmod1cl	$⊢ W \in LMod \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
16	15	ad2antrr	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
17		simprl	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to X \in U$
18		simprr	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to Y \in U$
19	7 14 1 8 2	lsscl	$⊢ (U \in S \land (1_{Scalar (W)} \in {Base}_{Scalar (W)} \land X \in U \land Y \in U)) \to (1_{Scalar (W)} \cdot_{W} X) \underset{˙}{+} Y \in U$
20	13 16 17 18 19	syl13anc	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to (1_{Scalar (W)} \cdot_{W} X) \underset{˙}{+} Y \in U$
21	12 20	eqeltrrd	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to X \underset{˙}{+} Y \in U$

Metamath Proof Explorer

Theorem lssvacl

Proof