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