Metamath Proof Explorer

Theorem nvpncan2

Description: Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nvpncan2.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvpncan2.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 nvpncan2.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
4 simp1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑈 ∈ NrmCVec )
5 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
6 simp2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
7 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
8 1 2 7 3 nvmval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐴 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
9 4 5 6 8 syl3anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐴 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
10 simp3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
11 neg1cn ⊢ - 1 ∈ ℂ
12 1 7 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
13 11 12 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
14 13 3adant3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
15 1 2 nvadd32 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) 𝐺 𝐵 ) )
16 4 6 10 14 15 syl13anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) 𝐺 𝐵 ) )
17 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
18 1 2 7 17 nvrinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( 0vec ‘ 𝑈 ) )
19 18 3adant3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( 0vec ‘ 𝑈 ) )
20 19 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) 𝐺 𝐵 ) = ( ( 0vec ‘ 𝑈 ) 𝐺 𝐵 ) )
21 1 2 17 nv0lid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝐺 𝐵 ) = 𝐵 )
22 21 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝐺 𝐵 ) = 𝐵 )
23 20 22 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) 𝐺 𝐵 ) = 𝐵 )
24 16 23 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = 𝐵 )
25 9 24 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐴 ) = 𝐵 )