Theorem ldualssvsubcl

Description: Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015)

	Ref	Expression
Hypotheses	ldualssvsubcl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualssvsubcl.m	$$⊢\underset{\dot{}}{-}={-}_D$$
	ldualssvsubcl.s	$$⊢S=\mathrm{LSubSp}\left(D\right)$$
	ldualssvsubcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualssvsubcl.u	$$⊢\phi \to U\in S$$
	ldualssvsubcl.x	$$⊢\phi \to X\in U$$
	ldualssvsubcl.y	$$⊢\phi \to Y\in U$$
Assertion	ldualssvsubcl	$$⊢\phi \to X\underset{\dot{}}{-}Y\in U$$

Proof

Step	Hyp	Ref	Expression
1		ldualssvsubcl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
2		ldualssvsubcl.m	$$⊢\underset{\dot{}}{-}={-}_D$$
3		ldualssvsubcl.s	$$⊢S=\mathrm{LSubSp}\left(D\right)$$
4		ldualssvsubcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		ldualssvsubcl.u	$$⊢\phi \to U\in S$$
6		ldualssvsubcl.x	$$⊢\phi \to X\in U$$
7		ldualssvsubcl.y	$$⊢\phi \to Y\in U$$
8	1 4	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
9	2 3	lssvsubcl	$$⊢\left(\left(D\in \mathrm{LMod}\wedge U\in S\right)\wedge \left(X\in U\wedge Y\in U\right)\right)\to X\underset{\dot{}}{-}Y\in U$$
10	8 5 6 7 9	syl22anc	$$⊢\phi \to X\underset{\dot{}}{-}Y\in U$$