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 𝑥 ) ) )