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

Metamath Proof Explorer

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 = + ℎ ⋅ ℎ norm ℎ
h2h.2 ⊢ U ∈ NrmCVec
h2h.4 ⊢ ℋ = BaseSet ⁡ U
Assertion h2hvs ⊢ - ℎ = - v ⁡ U

Proof

Step Hyp Ref Expression
1 h2h.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 h2h.2 ⊢ U ∈ NrmCVec
3 h2h.4 ⊢ ℋ = BaseSet ⁡ U
4 df-hvsub ⊢ - ℎ = x ∈ ℋ , y ∈ ℋ ⟼ x + ℎ -1 ⋅ ℎ y
5 1 2 h2hva ⊢ + ℎ = + v ⁡ U
6 1 2 h2hsm ⊢ ⋅ ℎ = ⋅ 𝑠OLD ⁡ U
7 eqid ⊢ - v ⁡ U = - v ⁡ U
8 3 5 6 7 nvmfval ⊢ U ∈ NrmCVec → - v ⁡ U = x ∈ ℋ , y ∈ ℋ ⟼ x + ℎ -1 ⋅ ℎ y
9 2 8 ax-mp ⊢ - v ⁡ U = x ∈ ℋ , y ∈ ℋ ⟼ x + ℎ -1 ⋅ ℎ y
10 4 9 eqtr4i ⊢ - ℎ = - v ⁡ U