This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑈 )