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

Metamath Proof Explorer

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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 𝑁 𝐵 ) )