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

Metamath Proof Explorer

Theorem h2hva

Description: The group (addition) 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 h2hva ⊢ + ℎ = + v ⁡ U

Proof

Step Hyp Ref Expression
1 h2h.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 h2h.2 ⊢ U ∈ NrmCVec
3 eqid ⊢ + v ⁡ + ℎ ⋅ ℎ norm ℎ = + v ⁡ + ℎ ⋅ ℎ norm ℎ
4 3 vafval ⊢ + v ⁡ + ℎ ⋅ ℎ norm ℎ = 1 st ⁡ 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 ⊢ 1 st ⁡ 1 st ⁡ + ℎ ⋅ ℎ norm ℎ = 1 st ⁡ + ℎ ⋅ ℎ
12 8 simp1i ⊢ + ℎ ∈ V
13 8 simp2i ⊢ ⋅ ℎ ∈ V
14 12 13 op1st ⊢ 1 st ⁡ + ℎ ⋅ ℎ = + ℎ
15 4 11 14 3eqtrri ⊢ + ℎ = + v ⁡ + ℎ ⋅ ℎ norm ℎ
16 1 fveq2i ⊢ + v ⁡ U = + v ⁡ + ℎ ⋅ ℎ norm ℎ
17 15 16 eqtr4i ⊢ + ℎ = + v ⁡ U