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)$$