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

Metamath Proof Explorer

Definition df-hnorm

Description: Define the function for the norm of a vector of Hilbert space. See normval for its value and normcl for its closure. Theorems norm-i-i , norm-ii-i , and norm-iii-i show it has the expected properties of a norm. In the literature, the norm of A is usually written "|| A ||", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in Beran p. 96. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

Ref Expression
Assertion df-hnorm ⊢ norm ℎ = x ∈ dom ⁡ dom ⁡ ⋅ ih ⟼ x ⋅ ih x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cno class norm ℎ
1 vx setvar x
2 csp class ⋅ ih
3 2 cdm class dom ⁡ ⋅ ih
4 3 cdm class dom ⁡ dom ⁡ ⋅ ih
5 csqrt class √
6 1 cv setvar x
7 6 6 2 co class x ⋅ ih x
8 7 5 cfv class x ⋅ ih x
9 1 4 8 cmpt class x ∈ dom ⁡ dom ⁡ ⋅ ih ⟼ x ⋅ ih x
10 0 9 wceq wff norm ℎ = x ∈ dom ⁡ dom ⁡ ⋅ ih ⟼ x ⋅ ih x