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 𝑆 𝐵 ) 𝐺 𝐴 ) )