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

Metamath Proof Explorer

Theorem hodseqi

Description: Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses hodseq.2 ⊢ S : ℋ ⟶ ℋ
hodseq.3 ⊢ T : ℋ ⟶ ℋ
Assertion hodseqi ⊢ S + op T - op S = T

Proof

Step Hyp Ref Expression
1 hodseq.2 ⊢ S : ℋ ⟶ ℋ
2 hodseq.3 ⊢ T : ℋ ⟶ ℋ
3 eqid ⊢ T - op S = T - op S
4 2 1 hosubcli ⊢ T - op S : ℋ ⟶ ℋ
5 2 1 4 hodsi ⊢ T - op S = T - op S ↔ S + op T - op S = T
6 3 5 mpbi ⊢ S + op T - op S = T