Theorem pjmf1

Description: The projector function maps one-to-one into the set of Hilbert space operators. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjmf1	$$⊢{\mathrm{proj}}_{ℎ}:{\mathbf{C}}_{\mathscr{H}}\underset{1-1}{⟶}{\mathscr{H}}^{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		pjmfn	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}$$
2		pjhf	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(x\right):\mathscr{H}⟶\mathscr{H}$$
3		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
4	3 3	elmap	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)\in \left({\mathscr{H}}^{\mathscr{H}}\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(x\right):\mathscr{H}⟶\mathscr{H}$$
5	2 4	sylibr	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(x\right)\in \left({\mathscr{H}}^{\mathscr{H}}\right)$$
6	5	rgen	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}{\mathrm{proj}}_{ℎ}\left(x\right)\in \left({\mathscr{H}}^{\mathscr{H}}\right)$$
7		ffnfv	$$⊢{\mathrm{proj}}_{ℎ}:{\mathbf{C}}_{\mathscr{H}}⟶{\mathscr{H}}^{\mathscr{H}}\leftrightarrow \left({\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}{\mathrm{proj}}_{ℎ}\left(x\right)\in \left({\mathscr{H}}^{\mathscr{H}}\right)\right)$$
8	1 6 7	mpbir2an	$$⊢{\mathrm{proj}}_{ℎ}:{\mathbf{C}}_{\mathscr{H}}⟶{\mathscr{H}}^{\mathscr{H}}$$
9		pj11	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(y\right)\leftrightarrow x=y\right)$$
10	9	biimpd	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(y\right)\to x=y\right)$$
11	10	rgen2	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left({\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(y\right)\to x=y\right)$$
12		dff13	$$⊢{\mathrm{proj}}_{ℎ}:{\mathbf{C}}_{\mathscr{H}}\underset{1-1}{⟶}{\mathscr{H}}^{\mathscr{H}}\leftrightarrow \left({\mathrm{proj}}_{ℎ}:{\mathbf{C}}_{\mathscr{H}}⟶{\mathscr{H}}^{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left({\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(y\right)\to x=y\right)\right)$$
13	8 11 12	mpbir2an	$$⊢{\mathrm{proj}}_{ℎ}:{\mathbf{C}}_{\mathscr{H}}\underset{1-1}{⟶}{\mathscr{H}}^{\mathscr{H}}$$