Theorem ldualssvsubcl

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

	Ref	Expression
Hypotheses	ldualssvsubcl.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualssvsubcl.m	⊢ − = ( -g ‘ 𝐷 )
	ldualssvsubcl.s	⊢ 𝑆 = ( LSubSp ‘ 𝐷 )
	ldualssvsubcl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	ldualssvsubcl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	ldualssvsubcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
	ldualssvsubcl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion	ldualssvsubcl	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ldualssvsubcl.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
2		ldualssvsubcl.m	⊢ − = ( -g ‘ 𝐷 )
3		ldualssvsubcl.s	⊢ 𝑆 = ( LSubSp ‘ 𝐷 )
4		ldualssvsubcl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		ldualssvsubcl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		ldualssvsubcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
7		ldualssvsubcl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
8	1 4	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
9	2 3	lssvsubcl	⊢ ( ( ( 𝐷 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 − 𝑌 ) ∈ 𝑈 )
10	8 5 6 7 9	syl22anc	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ 𝑈 )