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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lmodvsubval2.p	⊢ + = ( +g ‘ 𝑊 )
	lmodvsubval2.m	⊢ − = ( -g ‘ 𝑊 )
	lmodvsubval2.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lmodvsubval2.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lmodvsubval2.n	⊢ 𝑁 = ( invg ‘ 𝐹 )
	lmodvsubval2.u	⊢ 1 = ( 1r ‘ 𝐹 )
Assertion	lmodvsubval2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( 𝑁 ‘ 1 ) · 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmodvsubval2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lmodvsubval2.p	⊢ + = ( +g ‘ 𝑊 )
3		lmodvsubval2.m	⊢ − = ( -g ‘ 𝑊 )
4		lmodvsubval2.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		lmodvsubval2.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		lmodvsubval2.n	⊢ 𝑁 = ( invg ‘ 𝐹 )
7		lmodvsubval2.u	⊢ 1 = ( 1r ‘ 𝐹 )
8		eqid	⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
9	1 2 8 3	grpsubval	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) ) )
10	9	3adant1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) ) )
11	1 8 4 5 7 6	lmodvneg1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑁 ‘ 1 ) · 𝐵 ) = ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) )
12	11	3adant2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑁 ‘ 1 ) · 𝐵 ) = ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) )
13	12	oveq2d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + ( ( 𝑁 ‘ 1 ) · 𝐵 ) ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) ) )
14	10 13	eqtr4d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( 𝑁 ‘ 1 ) · 𝐵 ) ) )