Theorem hoaddid1i

Description: Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hoaddid1.1	|- T : ~H --> ~H
Assertion	hoaddid1i	|- ( T +op 0hop ) = T

Proof

Step	Hyp	Ref	Expression
1		hoaddid1.1	|- T : ~H --> ~H
2		ho0f	|- 0hop : ~H --> ~H
3		hosval	|- ( ( T : ~H --> ~H /\ 0hop : ~H --> ~H /\ x e. ~H ) -> ( ( T +op 0hop ) ` x ) = ( ( T ` x ) +h ( 0hop ` x ) ) )
4	1 2 3	mp3an12	|- ( x e. ~H -> ( ( T +op 0hop ) ` x ) = ( ( T ` x ) +h ( 0hop ` x ) ) )
5		ho0val	|- ( x e. ~H -> ( 0hop ` x ) = 0h )
6	5	oveq2d	|- ( x e. ~H -> ( ( T ` x ) +h ( 0hop ` x ) ) = ( ( T ` x ) +h 0h ) )
7	1	ffvelrni	|- ( x e. ~H -> ( T ` x ) e. ~H )
8		ax-hvaddid	|- ( ( T ` x ) e. ~H -> ( ( T ` x ) +h 0h ) = ( T ` x ) )
9	7 8	syl	|- ( x e. ~H -> ( ( T ` x ) +h 0h ) = ( T ` x ) )
10	4 6 9	3eqtrd	|- ( x e. ~H -> ( ( T +op 0hop ) ` x ) = ( T ` x ) )
11	10	rgen	|- A. x e. ~H ( ( T +op 0hop ) ` x ) = ( T ` x )
12	1 2	hoaddcli	|- ( T +op 0hop ) : ~H --> ~H
13	12 1	hoeqi	|- ( A. x e. ~H ( ( T +op 0hop ) ` x ) = ( T ` x ) <-> ( T +op 0hop ) = T )
14	11 13	mpbi	|- ( T +op 0hop ) = T