Metamath Proof Explorer


Theorem dfhnorm2

Description: Alternate definition of the norm of a vector of Hilbert space. Definition of norm in Beran p. 96. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion dfhnorm2 norm = ( 𝑥 ∈ ℋ ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 df-hnorm norm = ( 𝑥 ∈ dom dom ·ih ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )
2 ax-hfi ·ih : ( ℋ × ℋ ) ⟶ ℂ
3 2 fdmi dom ·ih = ( ℋ × ℋ )
4 3 dmeqi dom dom ·ih = dom ( ℋ × ℋ )
5 dmxpid dom ( ℋ × ℋ ) = ℋ
6 4 5 eqtr2i ℋ = dom dom ·ih
7 6 mpteq1i ( 𝑥 ∈ ℋ ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) ) = ( 𝑥 ∈ dom dom ·ih ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )
8 1 7 eqtr4i norm = ( 𝑥 ∈ ℋ ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )