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

Metamath Proof Explorer

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	$⊢ {proj}_{ℎ} : C_{ℋ} \underset{1-1}{⟶} ℋ^{ℋ}$

Proof

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