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_ℋ –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 ℋ )