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

Metamath Proof Explorer

Theorem ho0coi

Description: Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006) (New usage is discouraged.)

Ref Expression
Hypothesis hoaddrid.1 
|- T : ~H --> ~H
Assertion ho0coi 
|- ( 0hop o. T ) = 0hop

Proof

Step Hyp Ref Expression
1 hoaddrid.1 
 |-  T : ~H --> ~H
2 1 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
3 ho0val 
 |-  ( ( T ` x ) e. ~H -> ( 0hop ` ( T ` x ) ) = 0h )
4 2 3 syl 
 |-  ( x e. ~H -> ( 0hop ` ( T ` x ) ) = 0h )
5 ho0f 
 |-  0hop : ~H --> ~H
6 5 1 hocoi 
 |-  ( x e. ~H -> ( ( 0hop o. T ) ` x ) = ( 0hop ` ( T ` x ) ) )
7 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
8 4 6 7 3eqtr4d 
 |-  ( x e. ~H -> ( ( 0hop o. T ) ` x ) = ( 0hop ` x ) )
9 8 rgen 
 |-  A. x e. ~H ( ( 0hop o. T ) ` x ) = ( 0hop ` x )
10 5 1 hocofi 
 |-  ( 0hop o. T ) : ~H --> ~H
11 10 5 hoeqi 
 |-  ( A. x e. ~H ( ( 0hop o. T ) ` x ) = ( 0hop ` x ) <-> ( 0hop o. T ) = 0hop )
12 9 11 mpbi 
 |-  ( 0hop o. T ) = 0hop