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 ⊢ 𝑆 : ℋ ⟶ ℋ
hodseq.3 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion hodseqi ( 𝑆 +op ( 𝑇 −op 𝑆 ) ) = 𝑇

Proof

Step Hyp Ref Expression
1 hodseq.2 ⊢ 𝑆 : ℋ ⟶ ℋ
2 hodseq.3 ⊢ 𝑇 : ℋ ⟶ ℋ
3 eqid ⊢ ( 𝑇 −op 𝑆 ) = ( 𝑇 −op 𝑆 )
4 2 1 hosubcli ⊢ ( 𝑇 −op 𝑆 ) : ℋ ⟶ ℋ
5 2 1 4 hodsi ⊢ ( ( 𝑇 −op 𝑆 ) = ( 𝑇 −op 𝑆 ) ↔ ( 𝑆 +op ( 𝑇 −op 𝑆 ) ) = 𝑇 )
6 3 5 mpbi ⊢ ( 𝑆 +op ( 𝑇 −op 𝑆 ) ) = 𝑇