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

Metamath Proof Explorer

Theorem dfiop2

Description: Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion dfiop2 Iop = ( I ↾ ℋ )

Proof

Step Hyp Ref Expression
1 df-iop ⊢ Iop = ( projℎ ‘ ℋ )
2 helch ⊢ ℋ ∈ Cℋ
3 2 pjfni ⊢ ( projℎ ‘ ℋ ) Fn ℋ
4 fnresi ⊢ ( I ↾ ℋ ) Fn ℋ
5 pjch1 ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) = 𝑥 )
6 fvresi ⊢ ( 𝑥 ∈ ℋ → ( ( I ↾ ℋ ) ‘ 𝑥 ) = 𝑥 )
7 5 6 eqtr4d ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) = ( ( I ↾ ℋ ) ‘ 𝑥 ) )
8 7 rgen ⊢ ∀ 𝑥 ∈ ℋ ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) = ( ( I ↾ ℋ ) ‘ 𝑥 )
9 eqfnfv ⊢ ( ( ( projℎ ‘ ℋ ) Fn ℋ ∧ ( I ↾ ℋ ) Fn ℋ ) → ( ( projℎ ‘ ℋ ) = ( I ↾ ℋ ) ↔ ∀ 𝑥 ∈ ℋ ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) = ( ( I ↾ ℋ ) ‘ 𝑥 ) ) )
10 8 9 mpbiri ⊢ ( ( ( projℎ ‘ ℋ ) Fn ℋ ∧ ( I ↾ ℋ ) Fn ℋ ) → ( projℎ ‘ ℋ ) = ( I ↾ ℋ ) )
11 3 4 10 mp2an ⊢ ( projℎ ‘ ℋ ) = ( I ↾ ℋ )
12 1 11 eqtri ⊢ Iop = ( I ↾ ℋ )