ldualssvsubcl

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

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

Metamath Proof Explorer