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

Metamath Proof Explorer

Theorem h2hsm

Description: The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008) (New usage is discouraged.)

Ref Expression
Hypotheses h2h.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
h2h.2 ⊢ U ∈ NrmCVec
Assertion h2hsm ⊢ ⋅ ℎ = ⋅ 𝑠OLD ⁡ U

Proof

Step Hyp Ref Expression
1 h2h.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 h2h.2 ⊢ U ∈ NrmCVec
3 eqid ⊢ ⋅ 𝑠OLD ⁡ + ℎ ⋅ ℎ norm ℎ = ⋅ 𝑠OLD ⁡ + ℎ ⋅ ℎ norm ℎ
4 3 smfval ⊢ ⋅ 𝑠OLD ⁡ + ℎ ⋅ ℎ norm ℎ = 2 nd ⁡ 1 st ⁡ + ℎ ⋅ ℎ norm ℎ
5 opex ⊢ + ℎ ⋅ ℎ ∈ V
6 1 2 eqeltrri ⊢ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec
7 nvex ⊢ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec → + ℎ ∈ V ∧ ⋅ ℎ ∈ V ∧ norm ℎ ∈ V
8 6 7 ax-mp ⊢ + ℎ ∈ V ∧ ⋅ ℎ ∈ V ∧ norm ℎ ∈ V
9 8 simp3i ⊢ norm ℎ ∈ V
10 5 9 op1st ⊢ 1 st ⁡ + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ
11 10 fveq2i ⊢ 2 nd ⁡ 1 st ⁡ + ℎ ⋅ ℎ norm ℎ = 2 nd ⁡ + ℎ ⋅ ℎ
12 8 simp1i ⊢ + ℎ ∈ V
13 8 simp2i ⊢ ⋅ ℎ ∈ V
14 12 13 op2nd ⊢ 2 nd ⁡ + ℎ ⋅ ℎ = ⋅ ℎ
15 4 11 14 3eqtrri ⊢ ⋅ ℎ = ⋅ 𝑠OLD ⁡ + ℎ ⋅ ℎ norm ℎ
16 1 fveq2i ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ + ℎ ⋅ ℎ norm ℎ
17 15 16 eqtr4i ⊢ ⋅ ℎ = ⋅ 𝑠OLD ⁡ U