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

Metamath Proof Explorer

Theorem hosd1i

Description: Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses hosd1.2 
|- T : ~H --> ~H
hosd1.3 
|- U : ~H --> ~H
Assertion hosd1i 
|- ( T +op U ) = ( T -op ( 0hop -op U ) )

Proof

Step Hyp Ref Expression
1 hosd1.2 
 |-  T : ~H --> ~H
2 hosd1.3 
 |-  U : ~H --> ~H
3 ho0f 
 |-  0hop : ~H --> ~H
4 3 2 hosubcli 
 |-  ( 0hop -op U ) : ~H --> ~H
5 1 2 hoaddcli 
 |-  ( T +op U ) : ~H --> ~H
6 4 5 hoaddcomi 
 |-  ( ( 0hop -op U ) +op ( T +op U ) ) = ( ( T +op U ) +op ( 0hop -op U ) )
7 5 3 2 hoaddsubassi 
 |-  ( ( ( T +op U ) +op 0hop ) -op U ) = ( ( T +op U ) +op ( 0hop -op U ) )
8 6 7 eqtr4i 
 |-  ( ( 0hop -op U ) +op ( T +op U ) ) = ( ( ( T +op U ) +op 0hop ) -op U )
9 5 hoaddridi 
 |-  ( ( T +op U ) +op 0hop ) = ( T +op U )
10 9 oveq1i 
 |-  ( ( ( T +op U ) +op 0hop ) -op U ) = ( ( T +op U ) -op U )
11 1 2 2 hoaddsubi 
 |-  ( ( T +op U ) -op U ) = ( ( T -op U ) +op U )
12 1 2 hosubcli 
 |-  ( T -op U ) : ~H --> ~H
13 12 2 hoaddcomi 
 |-  ( ( T -op U ) +op U ) = ( U +op ( T -op U ) )
14 2 1 hodseqi 
 |-  ( U +op ( T -op U ) ) = T
15 11 13 14 3eqtri 
 |-  ( ( T +op U ) -op U ) = T
16 8 10 15 3eqtri 
 |-  ( ( 0hop -op U ) +op ( T +op U ) ) = T
17 1 4 5 hodsi 
 |-  ( ( T -op ( 0hop -op U ) ) = ( T +op U ) <-> ( ( 0hop -op U ) +op ( T +op U ) ) = T )
18 16 17 mpbir 
 |-  ( T -op ( 0hop -op U ) ) = ( T +op U )
19 18 eqcomi 
 |-  ( T +op U ) = ( T -op ( 0hop -op U ) )