Theorem nvm

Description: Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvm.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvm.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	nvm.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	nvm.6	⊢ 𝑁 = ( /𝑔 ‘ 𝐺 )
Assertion	nvm	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 𝑁 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nvm.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvm.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3		nvm.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
4		nvm.6	⊢ 𝑁 = ( /𝑔 ‘ 𝐺 )
5	2 3	vsfval	⊢ 𝑀 = ( /𝑔 ‘ 𝐺 )
6	5 4	eqtr4i	⊢ 𝑀 = 𝑁
7	6	oveqi	⊢ ( 𝐴 𝑀 𝐵 ) = ( 𝐴 𝑁 𝐵 )
8	7	a1i	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 𝑁 𝐵 ) )