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

Proof

Step	Hyp	Ref	Expression
1		h2h.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		h2h.2	$$⊢U\in \mathrm{NrmCVec}$$
3		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)={\cdot }_{\mathrm{𝑠OLD}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
4	3	smfval	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)=2^{nd}\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	$$⊢2^{nd}\left(1^{st}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)=2^{nd}\left(⟨{+}_{ℎ},{\cdot }_{ℎ}⟩\right)$$
12	8	simp1i	$$⊢{+}_{ℎ}\in \mathrm{V}$$
13	8	simp2i	$$⊢{\cdot }_{ℎ}\in \mathrm{V}$$
14	12 13	op2nd	$$⊢2^{nd}\left(⟨{+}_{ℎ},{\cdot }_{ℎ}⟩\right)={\cdot }_{ℎ}$$
15	4 11 14	3eqtrri	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
16	1	fveq2i	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)={\cdot }_{\mathrm{𝑠OLD}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
17	15 16	eqtr4i	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$