Theorem hilims

Description: Hilbert space distance metric. (Contributed by NM, 13-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hilims.1	⊢ ℋ = ( BaseSet ‘ 𝑈 )
	hilims.2	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
	hilims.3	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
	hilims.5	⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )
	hilims.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	hilims.9	⊢ 𝑈 ∈ NrmCVec
Assertion	hilims	⊢ 𝐷 = ( normℎ ∘ −ℎ )

Proof

Step	Hyp	Ref	Expression
1		hilims.1	⊢ ℋ = ( BaseSet ‘ 𝑈 )
2		hilims.2	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
3		hilims.3	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
4		hilims.5	⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )
5		hilims.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
6		hilims.9	⊢ 𝑈 ∈ NrmCVec
7	1 2 3 4 6	hilhhi	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
8	7 5	hhims2	⊢ 𝐷 = ( normℎ ∘ −ℎ )