Theorem h2hvs

Description: The vector subtraction operation of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h2h.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	h2h.2	⊢ 𝑈 ∈ NrmCVec
	h2h.4	⊢ ℋ = ( BaseSet ‘ 𝑈 )
Assertion	h2hvs	⊢ −ℎ = ( −𝑣 ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		h2h.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		h2h.2	⊢ 𝑈 ∈ NrmCVec
3		h2h.4	⊢ ℋ = ( BaseSet ‘ 𝑈 )
4		df-hvsub	⊢ −ℎ = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
5	1 2	h2hva	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
6	1 2	h2hsm	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
7		eqid	⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
8	3 5 6 7	nvmfval	⊢ ( 𝑈 ∈ NrmCVec → ( −𝑣 ‘ 𝑈 ) = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) )
9	2 8	ax-mp	⊢ ( −𝑣 ‘ 𝑈 ) = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
10	4 9	eqtr4i	⊢ −ℎ = ( −𝑣 ‘ 𝑈 )