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

Metamath Proof Explorer

Theorem hoid1ri

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

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

Proof

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