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\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$

Proof

Step	Hyp	Ref	Expression
1		oveq12	$$⊢\left(x=A\wedge x=A\right)\to x{\cdot }_{\mathrm{ih}}x=A{\cdot }_{\mathrm{ih}}A$$
2	1	anidms	$$⊢x=A\to x{\cdot }_{\mathrm{ih}}x=A{\cdot }_{\mathrm{ih}}A$$
3	2	fveq2d	$$⊢x=A\to \sqrt{x{\cdot }_{\mathrm{ih}}x}=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
4		dfhnorm2	$$⊢{norm}_{ℎ}=\left(x\in \mathscr{H}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)$$
5		fvex	$$⊢\sqrt{A{\cdot }_{\mathrm{ih}}A}\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$