Theorem ldualssvsubcl

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

	Ref	Expression
Hypotheses	ldualssvsubcl.d	|- D = ( LDual ` W )
	ldualssvsubcl.m	|- .- = ( -g ` D )
	ldualssvsubcl.s	|- S = ( LSubSp ` D )
	ldualssvsubcl.w	|- ( ph -> W e. LMod )
	ldualssvsubcl.u	|- ( ph -> U e. S )
	ldualssvsubcl.x	|- ( ph -> X e. U )
	ldualssvsubcl.y	|- ( ph -> Y e. U )
Assertion	ldualssvsubcl	|- ( ph -> ( X .- Y ) e. U )

Proof

Step	Hyp	Ref	Expression
1		ldualssvsubcl.d	|- D = ( LDual ` W )
2		ldualssvsubcl.m	|- .- = ( -g ` D )
3		ldualssvsubcl.s	|- S = ( LSubSp ` D )
4		ldualssvsubcl.w	|- ( ph -> W e. LMod )
5		ldualssvsubcl.u	|- ( ph -> U e. S )
6		ldualssvsubcl.x	|- ( ph -> X e. U )
7		ldualssvsubcl.y	|- ( ph -> Y e. U )
8	1 4	lduallmod	|- ( ph -> D e. LMod )
9	2 3	lssvsubcl	|- ( ( ( D e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .- Y ) e. U )
10	8 5 6 7 9	syl22anc	|- ( ph -> ( X .- Y ) e. U )