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 ⁡ U
hilnorm.2 ⊢ ⋅ ih = ⋅ 𝑖OLD ⁡ U
hilnorm.9 ⊢ U ∈ NrmCVec
Assertion hilnormi ⊢ norm ℎ = norm CV ⁡ U

Proof

Step Hyp Ref Expression
1 hilnorm.5 ⊢ ℋ = BaseSet ⁡ U
2 hilnorm.2 ⊢ ⋅ ih = ⋅ 𝑖OLD ⁡ U
3 hilnorm.9 ⊢ U ∈ NrmCVec
4 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
5 1 4 2 ipnm ⊢ U ∈ NrmCVec ∧ x ∈ ℋ → norm CV ⁡ U ⁡ x = x ⋅ ih x
6 3 5 mpan ⊢ x ∈ ℋ → norm CV ⁡ U ⁡ x = x ⋅ ih x
7 6 mpteq2ia ⊢ x ∈ ℋ ⟼ norm CV ⁡ U ⁡ x = x ∈ ℋ ⟼ x ⋅ ih x
8 1 4 nvf ⊢ U ∈ NrmCVec → norm CV ⁡ U : ℋ ⟶ ℝ
9 8 feqmptd ⊢ U ∈ NrmCVec → norm CV ⁡ U = x ∈ ℋ ⟼ norm CV ⁡ U ⁡ x
10 3 9 ax-mp ⊢ norm CV ⁡ U = x ∈ ℋ ⟼ norm CV ⁡ U ⁡ x
11 dfhnorm2 ⊢ norm ℎ = x ∈ ℋ ⟼ x ⋅ ih x
12 7 10 11 3eqtr4ri ⊢ norm ℎ = norm CV ⁡ U