This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmodvsubcl

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

	Ref	Expression
Hypotheses	lmodvsubcl.v	$⊢ V = {Base}_{W}$
	lmodvsubcl.m	$⊢ \underset{˙}{-} = -_{W}$
Assertion	lmodvsubcl	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{-} Y \in V$

Step	Hyp	Ref	Expression
1		lmodvsubcl.v	$⊢ V = {Base}_{W}$
2		lmodvsubcl.m	$⊢ \underset{˙}{-} = -_{W}$
3		lmodgrp	$⊢ W \in LMod \to W \in Grp$
4	1 2	grpsubcl	$⊢ (W \in Grp \land X \in V \land Y \in V) \to X \underset{˙}{-} Y \in V$
5	3 4	syl3an1	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{-} Y \in V$