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ℋ –1-1→ ( ℋ ↑m ℋ )

Proof

Step	Hyp	Ref	Expression
1		pjmfn	⊢ projℎ Fn Cℋ
2		pjhf	⊢ ( 𝑥 ∈ Cℋ → ( projℎ ‘ 𝑥 ) : ℋ ⟶ ℋ )
3		ax-hilex	⊢ ℋ ∈ V
4	3 3	elmap	⊢ ( ( projℎ ‘ 𝑥 ) ∈ ( ℋ ↑m ℋ ) ↔ ( projℎ ‘ 𝑥 ) : ℋ ⟶ ℋ )
5	2 4	sylibr	⊢ ( 𝑥 ∈ Cℋ → ( projℎ ‘ 𝑥 ) ∈ ( ℋ ↑m ℋ ) )
6	5	rgen	⊢ ∀ 𝑥 ∈ Cℋ ( projℎ ‘ 𝑥 ) ∈ ( ℋ ↑m ℋ )
7		ffnfv	⊢ ( projℎ : Cℋ ⟶ ( ℋ ↑m ℋ ) ↔ ( projℎ Fn Cℋ ∧ ∀ 𝑥 ∈ Cℋ ( projℎ ‘ 𝑥 ) ∈ ( ℋ ↑m ℋ ) ) )
8	1 6 7	mpbir2an	⊢ projℎ : Cℋ ⟶ ( ℋ ↑m ℋ )
9		pj11	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( ( projℎ ‘ 𝑥 ) = ( projℎ ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
10	9	biimpd	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( ( projℎ ‘ 𝑥 ) = ( projℎ ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
11	10	rgen2	⊢ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( projℎ ‘ 𝑥 ) = ( projℎ ‘ 𝑦 ) → 𝑥 = 𝑦 )
12		dff13	⊢ ( projℎ : Cℋ –1-1→ ( ℋ ↑m ℋ ) ↔ ( projℎ : Cℋ ⟶ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( projℎ ‘ 𝑥 ) = ( projℎ ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
13	8 11 12	mpbir2an	⊢ projℎ : Cℋ –1-1→ ( ℋ ↑m ℋ )