Theorem honpcani

Description: Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hosd1.2	⊢ 𝑇 : ℋ ⟶ ℋ
	hosd1.3	⊢ 𝑈 : ℋ ⟶ ℋ
Assertion	honpcani	⊢ ( ( 𝑇 −op 𝑈 ) +op 𝑈 ) = 𝑇

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	⊢ 𝑇 : ℋ ⟶ ℋ
2		hosd1.3	⊢ 𝑈 : ℋ ⟶ ℋ
3	1 2 2	hoaddsubi	⊢ ( ( 𝑇 +op 𝑈 ) −op 𝑈 ) = ( ( 𝑇 −op 𝑈 ) +op 𝑈 )
4	1 2	hopncani	⊢ ( ( 𝑇 +op 𝑈 ) −op 𝑈 ) = 𝑇
5	3 4	eqtr3i	⊢ ( ( 𝑇 −op 𝑈 ) +op 𝑈 ) = 𝑇