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	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	h2h.2	$$⊢U\in \mathrm{NrmCVec}$$
	h2h.4	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
Assertion	h2hvs	$$⊢{-}_{ℎ}={-}_v\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		h2h.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		h2h.2	$$⊢U\in \mathrm{NrmCVec}$$
3		h2h.4	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
4		df-hvsub	$$⊢{-}_{ℎ}=\left(x\in \mathscr{H},y\in \mathscr{H}⟼x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)\right)$$
5	1 2	h2hva	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
6	1 2	h2hsm	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
7		eqid	$$⊢{-}_v\left(U\right)={-}_v\left(U\right)$$
8	3 5 6 7	nvmfval	$$⊢U\in \mathrm{NrmCVec}\to {-}_v\left(U\right)=\left(x\in \mathscr{H},y\in \mathscr{H}⟼x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)\right)$$
9	2 8	ax-mp	$$⊢{-}_v\left(U\right)=\left(x\in \mathscr{H},y\in \mathscr{H}⟼x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)\right)$$
10	4 9	eqtr4i	$$⊢{-}_{ℎ}={-}_v\left(U\right)$$