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	hoaddid1.1	|- T : ~H --> ~H
Assertion	ho0coi	|- ( 0hop o. T ) = 0hop

Proof

Step	Hyp	Ref	Expression
1		hoaddid1.1	|- T : ~H --> ~H
2	1	ffvelrni	|- ( 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