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

Metamath Proof Explorer

Theorem hoaddridi

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

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

Proof

Step Hyp Ref Expression
1 hoaddrid.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 ffvelcdmi 
 |-  ( 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