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

Metamath Proof Explorer

Theorem normval

Description: The value of the norm of a vector in Hilbert space. Definition of norm in Beran p. 96. In the literature, the norm of A is usually written as "|| A ||", but we use function value notation to take advantage of our existing theorems about functions. (Contributed by NM, 29-May-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	normval	\|- ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq12	\|- ( ( x = A /\ x = A ) -> ( x .ih x ) = ( A .ih A ) )
2	1	anidms	\|- ( x = A -> ( x .ih x ) = ( A .ih A ) )
3	2	fveq2d	\|- ( x = A -> ( sqrt ` ( x .ih x ) ) = ( sqrt ` ( A .ih A ) ) )
4		dfhnorm2	\|- normh = ( x e. ~H \|-> ( sqrt ` ( x .ih x ) ) )
5		fvex	\|- ( sqrt ` ( A .ih A ) ) e. _V
6	3 4 5	fvmpt	\|- ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) )