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

Metamath Proof Explorer

Theorem dfhnorm2

Proof