Theorem hilnormi

Description: Hilbert space norm in terms of vector space norm. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hilnorm.5	⊢ ℋ = ( BaseSet ‘ 𝑈 )
	hilnorm.2	⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )
	hilnorm.9	⊢ 𝑈 ∈ NrmCVec
Assertion	hilnormi	⊢ normℎ = ( normCV ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		hilnorm.5	⊢ ℋ = ( BaseSet ‘ 𝑈 )
2		hilnorm.2	⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )
3		hilnorm.9	⊢ 𝑈 ∈ NrmCVec
4		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
5	1 4 2	ipnm	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℋ ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) = ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )
6	3 5	mpan	⊢ ( 𝑥 ∈ ℋ → ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) = ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )
7	6	mpteq2ia	⊢ ( 𝑥 ∈ ℋ ↦ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ℋ ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )
8	1 4	nvf	⊢ ( 𝑈 ∈ NrmCVec → ( normCV ‘ 𝑈 ) : ℋ ⟶ ℝ )
9	8	feqmptd	⊢ ( 𝑈 ∈ NrmCVec → ( normCV ‘ 𝑈 ) = ( 𝑥 ∈ ℋ ↦ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
10	3 9	ax-mp	⊢ ( normCV ‘ 𝑈 ) = ( 𝑥 ∈ ℋ ↦ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) )
11		dfhnorm2	⊢ normℎ = ( 𝑥 ∈ ℋ ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )
12	7 10 11	3eqtr4ri	⊢ normℎ = ( normCV ‘ 𝑈 )