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 𝑆 ) ) = 𝑇