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

Metamath Proof Explorer

Theorem hosd2i

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 : ℋ ⟶ ℋ
hosd1.3 ⊢ U : ℋ ⟶ ℋ
Assertion hosd2i ⊢ T + op U = T - op U - op U - op U

Proof

Step Hyp Ref Expression
1 hosd1.2 ⊢ T : ℋ ⟶ ℋ
2 hosd1.3 ⊢ U : ℋ ⟶ ℋ
3 1 2 hosd1i ⊢ T + op U = T - op 0 hop - op U
4 2 hodidi ⊢ U - op U = 0 hop
5 4 oveq1i ⊢ U - op U - op U = 0 hop - op U
6 5 oveq2i ⊢ T - op U - op U - op U = T - op 0 hop - op U
7 3 6 eqtr4i ⊢ T + op U = T - op U - op U - op U