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

Metamath Proof Explorer

Theorem nvmval2

Description: Value of vector subtraction on a normed complex vector space. (Contributed by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvmval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvmval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
nvmval.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvmval.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
Assertion nvmval2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nvmval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvmval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 nvmval.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 nvmval.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
5 1 2 3 4 nvmval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )
6 neg1cn ⊢ - 1 ∈ ℂ
7 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
8 6 7 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
9 8 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
10 1 2 nvcom ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) = ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) )
11 9 10 syld3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) = ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) )
12 5 11 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) )