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 : C1-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 : C1-1→ ( ℋ ↑m ℋ ) ↔ ( proj : C ⟶ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥C𝑦C ( ( proj𝑥 ) = ( proj𝑦 ) → 𝑥 = 𝑦 ) ) )
13 8 11 12 mpbir2an proj : C1-1→ ( ℋ ↑m ℋ )