Theorem hhims

Description: The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	hhims.2	⊢ 𝐷 = ( normℎ ∘ −ℎ )
Assertion	hhims	⊢ 𝐷 = ( IndMet ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hhims.2	⊢ 𝐷 = ( normℎ ∘ −ℎ )
3	1	hhnv	⊢ 𝑈 ∈ NrmCVec
4	1	hhvs	⊢ −ℎ = ( −𝑣 ‘ 𝑈 )
5	1	hhnm	⊢ normℎ = ( normCV ‘ 𝑈 )
6		eqid	⊢ ( IndMet ‘ 𝑈 ) = ( IndMet ‘ 𝑈 )
7	4 5 6	imsval	⊢ ( 𝑈 ∈ NrmCVec → ( IndMet ‘ 𝑈 ) = ( normℎ ∘ −ℎ ) )
8	3 7	ax-mp	⊢ ( IndMet ‘ 𝑈 ) = ( normℎ ∘ −ℎ )
9	2 8	eqtr4i	⊢ 𝐷 = ( IndMet ‘ 𝑈 )