Metamath Proof Explorer


Theorem nvpncan

Description: Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvpncan2.1 𝑋 = ( BaseSet ‘ 𝑈 )
nvpncan2.2 𝐺 = ( +𝑣𝑈 )
nvpncan2.3 𝑀 = ( −𝑣𝑈 )
Assertion nvpncan ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐵 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 nvpncan2.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvpncan2.2 𝐺 = ( +𝑣𝑈 )
3 nvpncan2.3 𝑀 = ( −𝑣𝑈 )
4 1 2 nvcom ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐴𝑋 ) → ( 𝐵 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐵 ) )
5 4 oveq1d ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐴𝑋 ) → ( ( 𝐵 𝐺 𝐴 ) 𝑀 𝐵 ) = ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐵 ) )
6 1 2 3 nvpncan2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐴𝑋 ) → ( ( 𝐵 𝐺 𝐴 ) 𝑀 𝐵 ) = 𝐴 )
7 5 6 eqtr3d ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐴𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐵 ) = 𝐴 )
8 7 3com23 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐵 ) = 𝐴 )