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

Metamath Proof Explorer

Theorem ho0subi

Description: Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hodseq.2 
|- S : ~H --> ~H
hodseq.3 
|- T : ~H --> ~H
Assertion ho0subi 
|- ( S -op T ) = ( S +op ( 0hop -op T ) )

Proof

Step Hyp Ref Expression
1 hodseq.2 
 |-  S : ~H --> ~H
2 hodseq.3 
 |-  T : ~H --> ~H
3 ho0f 
 |-  0hop : ~H --> ~H
4 3 2 hosubcli 
 |-  ( 0hop -op T ) : ~H --> ~H
5 2 1 4 hoadd12i 
 |-  ( T +op ( S +op ( 0hop -op T ) ) ) = ( S +op ( T +op ( 0hop -op T ) ) )
6 2 3 hodseqi 
 |-  ( T +op ( 0hop -op T ) ) = 0hop
7 6 oveq2i 
 |-  ( S +op ( T +op ( 0hop -op T ) ) ) = ( S +op 0hop )
8 1 hoaddridi 
 |-  ( S +op 0hop ) = S
9 5 7 8 3eqtri 
 |-  ( T +op ( S +op ( 0hop -op T ) ) ) = S
10 1 4 hoaddcli 
 |-  ( S +op ( 0hop -op T ) ) : ~H --> ~H
11 1 2 10 hodsi 
 |-  ( ( S -op T ) = ( S +op ( 0hop -op T ) ) <-> ( T +op ( S +op ( 0hop -op T ) ) ) = S )
12 9 11 mpbir 
 |-  ( S -op T ) = ( S +op ( 0hop -op T ) )