lssvsubcl

Description: Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lssvsubcl.m	$⊢ \underset{˙}{-} = -_{W}$
	lssvsubcl.s	$⊢ S = LSubSp (W)$
Assertion	lssvsubcl	$⊢ ((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		lssvsubcl.m	$⊢ \underset{˙}{-} = -_{W}$
2		lssvsubcl.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	4 2	lssel	$⊢ (U \in S \land Y \in U) \to Y \in {Base}_{W}$
8	7	ad2ant2l	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to Y \in {Base}_{W}$
9		eqid	$⊢ +_{W} = +_{W}$
10		eqid	$⊢ Scalar (W) = Scalar (W)$
11		eqid	$⊢ \cdot_{W} = \cdot_{W}$
12		eqid	$⊢ {inv}_{g} (Scalar (W)) = {inv}_{g} (Scalar (W))$
13		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
14	4 9 1 10 11 12 13	lmodvsubval2	$⊢ (W \in LMod \land X \in {Base}_{W} \land Y \in {Base}_{W}) \to X \underset{˙}{-} Y = X +_{W} ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y)$
15	3 6 8 14	syl3anc	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to X \underset{˙}{-} Y = X +_{W} ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y)$
16	10	lmodfgrp	$⊢ W \in LMod \to Scalar (W) \in Grp$
17	3 16	syl	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to Scalar (W) \in Grp$
18		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
19	10 18 13	lmod1cl	$⊢ W \in LMod \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
20	3 19	syl	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
21	18 12	grpinvcl	$⊢ (Scalar (W) \in Grp \land 1_{Scalar (W)} \in {Base}_{Scalar (W)}) \to {inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \in {Base}_{Scalar (W)}$
22	17 20 21	syl2anc	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to {inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \in {Base}_{Scalar (W)}$
23	4 10 11 18	lmodvscl	$⊢ (W \in LMod \land {inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \in {Base}_{Scalar (W)} \land Y \in {Base}_{W}) \to {inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y \in {Base}_{W}$
24	3 22 8 23	syl3anc	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to {inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y \in {Base}_{W}$
25	4 9	lmodcom	$⊢ (W \in LMod \land X \in {Base}_{W} \land {inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y \in {Base}_{W}) \to X +_{W} ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y) = ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y) +_{W} X$
26	3 6 24 25	syl3anc	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to X +_{W} ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y) = ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y) +_{W} X$
27		simplr	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to U \in S$
28		simprr	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to Y \in U$
29		simprl	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to X \in U$
30	10 18 9 11 2	lsscl	$⊢ (U \in S \land ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \in {Base}_{Scalar (W)} \land Y \in U \land X \in U)) \to ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y) +_{W} X \in U$
31	27 22 28 29 30	syl13anc	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y) +_{W} X \in U$
32	26 31	eqeltrd	$⊢ ((W \in LMod \land U \in S) \land (X \in U \land Y \in U)) \to X +_{W} ({inv}_{g} (Scalar (W)) (1_{Scalar (W)}) \cdot_{W} Y) \in U$
33	15 32	eqeltrd	$⊢ ((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 lssvsubcl

Proof