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