# 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}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
h2h.2 ${⊢}{U}\in \mathrm{NrmCVec}$
Assertion h2hva ${⊢}{+}_{ℎ}={+}_{v}\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 h2h.1 ${⊢}{U}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
2 h2h.2 ${⊢}{U}\in \mathrm{NrmCVec}$
3 eqid ${⊢}{+}_{v}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)={+}_{v}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
4 3 vafval ${⊢}{+}_{v}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)={1}^{st}\left({1}^{st}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)$
5 opex ${⊢}⟨{+}_{ℎ},{\cdot }_{ℎ}⟩\in \mathrm{V}$
6 1 2 eqeltrri ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$
7 nvex ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}\to \left({+}_{ℎ}\in \mathrm{V}\wedge {\cdot }_{ℎ}\in \mathrm{V}\wedge {norm}_{ℎ}\in \mathrm{V}\right)$
8 6 7 ax-mp ${⊢}\left({+}_{ℎ}\in \mathrm{V}\wedge {\cdot }_{ℎ}\in \mathrm{V}\wedge {norm}_{ℎ}\in \mathrm{V}\right)$
9 8 simp3i ${⊢}{norm}_{ℎ}\in \mathrm{V}$
10 5 9 op1st ${⊢}{1}^{st}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)=⟨{+}_{ℎ},{\cdot }_{ℎ}⟩$
11 10 fveq2i ${⊢}{1}^{st}\left({1}^{st}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)={1}^{st}\left(⟨{+}_{ℎ},{\cdot }_{ℎ}⟩\right)$
12 8 simp1i ${⊢}{+}_{ℎ}\in \mathrm{V}$
13 8 simp2i ${⊢}{\cdot }_{ℎ}\in \mathrm{V}$
14 12 13 op1st ${⊢}{1}^{st}\left(⟨{+}_{ℎ},{\cdot }_{ℎ}⟩\right)={+}_{ℎ}$
15 4 11 14 3eqtrri ${⊢}{+}_{ℎ}={+}_{v}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
16 1 fveq2i ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
17 15 16 eqtr4i ${⊢}{+}_{ℎ}={+}_{v}\left({U}\right)$