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	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	h2h.2	⊢ 𝑈 ∈ NrmCVec
Assertion	h2hsm	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		h2h.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		h2h.2	⊢ 𝑈 ∈ NrmCVec
3		eqid	⊢ ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
4	3	smfval	⊢ ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( 2nd ‘ ( 1st ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , 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	⊢ ( 1st ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ⟨ +ℎ , ·ℎ ⟩
11	10	fveq2i	⊢ ( 2nd ‘ ( 1st ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) = ( 2nd ‘ ⟨ +ℎ , ·ℎ ⟩ )
12	8	simp1i	⊢ +ℎ ∈ V
13	8	simp2i	⊢ ·ℎ ∈ V
14	12 13	op2nd	⊢ ( 2nd ‘ ⟨ +ℎ , ·ℎ ⟩ ) = ·ℎ
15	4 11 14	3eqtrri	⊢ ·ℎ = ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
16	1	fveq2i	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
17	15 16	eqtr4i	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )