Metamath Proof Explorer

Theorem hoival

Description: The value of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoival A I op A = A


Step Hyp Ref Expression
1 df-iop I op = proj
2 1 fveq1i I op A = proj A
3 pjch1 A proj A = A
4 2 3 syl5eq A I op A = A