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 ↾ ℋ )