Metamath Proof Explorer

Theorem hoid1i

Description: Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis hoaddid1.1 
|- T : ~H --> ~H
Assertion hoid1i 
|- ( T o. Iop ) = T

Proof

Step Hyp Ref Expression
1 hoaddid1.1 
 |-  T : ~H --> ~H
2 df-iop 
 |-  Iop = ( projh ` ~H )
3 2 coeq2i 
 |-  ( T o. Iop ) = ( T o. ( projh ` ~H ) )
4 helch 
 |-  ~H e. CH
5 4 pjfi 
 |-  ( projh ` ~H ) : ~H --> ~H
6 1 5 hocoi 
 |-  ( x e. ~H -> ( ( T o. ( projh ` ~H ) ) ` x ) = ( T ` ( ( projh ` ~H ) ` x ) ) )
7 pjch1 
 |-  ( x e. ~H -> ( ( projh ` ~H ) ` x ) = x )
8 7 fveq2d 
 |-  ( x e. ~H -> ( T ` ( ( projh ` ~H ) ` x ) ) = ( T ` x ) )
9 6 8 eqtrd 
 |-  ( x e. ~H -> ( ( T o. ( projh ` ~H ) ) ` x ) = ( T ` x ) )
10 9 rgen 
 |-  A. x e. ~H ( ( T o. ( projh ` ~H ) ) ` x ) = ( T ` x )
11 1 5 hocofi 
 |-  ( T o. ( projh ` ~H ) ) : ~H --> ~H
12 11 1 hoeqi 
 |-  ( A. x e. ~H ( ( T o. ( projh ` ~H ) ) ` x ) = ( T ` x ) <-> ( T o. ( projh ` ~H ) ) = T )
13 10 12 mpbi 
 |-  ( T o. ( projh ` ~H ) ) = T
14 3 13 eqtri 
 |-  ( T o. Iop ) = T