Metamath Proof Explorer

Theorem lmodvsubval2

Description: Value of vector subtraction in terms of addition. ( hvsubval analog.) (Contributed by NM, 31-Mar-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

		Ref	Expression
	Hypotheses	lmodvsubval2.v	$⊢ V = {Base}_{W}$
		lmodvsubval2.p	$⊢ \underset{˙}{+} = +_{W}$
		lmodvsubval2.m	$⊢ \underset{˙}{-} = -_{W}$
		lmodvsubval2.f	$⊢ F = Scalar (W)$
		lmodvsubval2.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
		lmodvsubval2.n	$⊢ N = {inv}_{g} (F)$
		lmodvsubval2.u	$⊢ \underset{˙}{1} = 1_{F}$
	Assertion	lmodvsubval2	$⊢ (W \in LMod \land A \in V \land B \in V) \to A \underset{˙}{-} B = A \underset{˙}{+} (N (\underset{˙}{1}) \underset{˙}{\cdot} B)$

Proof

Step	Hyp	Ref	Expression
1		lmodvsubval2.v	$⊢ V = {Base}_{W}$
2		lmodvsubval2.p	$⊢ \underset{˙}{+} = +_{W}$
3		lmodvsubval2.m	$⊢ \underset{˙}{-} = -_{W}$
4		lmodvsubval2.f	$⊢ F = Scalar (W)$
5		lmodvsubval2.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		lmodvsubval2.n	$⊢ N = {inv}_{g} (F)$
7		lmodvsubval2.u	$⊢ \underset{˙}{1} = 1_{F}$
8		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
9	1 2 8 3	grpsubval	$⊢ (A \in V \land B \in V) \to A \underset{˙}{-} B = A \underset{˙}{+} {inv}_{g} (W) (B)$
10	9	3adant1	$⊢ (W \in LMod \land A \in V \land B \in V) \to A \underset{˙}{-} B = A \underset{˙}{+} {inv}_{g} (W) (B)$
11	1 8 4 5 7 6	lmodvneg1	$⊢ (W \in LMod \land B \in V) \to N (\underset{˙}{1}) \underset{˙}{\cdot} B = {inv}_{g} (W) (B)$
12	11	3adant2	$⊢ (W \in LMod \land A \in V \land B \in V) \to N (\underset{˙}{1}) \underset{˙}{\cdot} B = {inv}_{g} (W) (B)$
13	12	oveq2d	$⊢ (W \in LMod \land A \in V \land B \in V) \to A \underset{˙}{+} (N (\underset{˙}{1}) \underset{˙}{\cdot} B) = A \underset{˙}{+} {inv}_{g} (W) (B)$
14	10 13	eqtr4d	$⊢ (W \in LMod \land A \in V \land B \in V) \to A \underset{˙}{-} B = A \underset{˙}{+} (N (\underset{˙}{1}) \underset{˙}{\cdot} B)$