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

Proof

Step	Hyp	Ref	Expression
1		df-hnorm	$$⊢{norm}_{ℎ}=\left(x\in \mathrm{dom}\mathrm{dom}{\cdot }_{\mathrm{ih}}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)$$
2		ax-hfi	$$⊢{\cdot }_{\mathrm{ih}}:\mathscr{H}\times \mathscr{H}⟶ℂ$$
3	2	fdmi	$$⊢\mathrm{dom}{\cdot }_{\mathrm{ih}}=\mathscr{H}\times \mathscr{H}$$
4	3	dmeqi	$$⊢\mathrm{dom}\mathrm{dom}{\cdot }_{\mathrm{ih}}=\mathrm{dom}\left(\mathscr{H}\times \mathscr{H}\right)$$
5		dmxpid	$$⊢\mathrm{dom}\left(\mathscr{H}\times \mathscr{H}\right)=\mathscr{H}$$
6	4 5	eqtr2i	$$⊢\mathscr{H}=\mathrm{dom}\mathrm{dom}{\cdot }_{\mathrm{ih}}$$
7	6	mpteq1i	$$⊢\left(x\in \mathscr{H}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)=\left(x\in \mathrm{dom}\mathrm{dom}{\cdot }_{\mathrm{ih}}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)$$
8	1 7	eqtr4i	$$⊢{norm}_{ℎ}=\left(x\in \mathscr{H}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)$$