Theorem hopncani

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

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

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	⊢ 𝑇 : ℋ ⟶ ℋ
2		hosd1.3	⊢ 𝑈 : ℋ ⟶ ℋ
3	1 2 2	hoaddsubassi	⊢ ( ( 𝑇 +op 𝑈 ) −op 𝑈 ) = ( 𝑇 +op ( 𝑈 −op 𝑈 ) )
4	2	hodidi	⊢ ( 𝑈 −op 𝑈 ) = 0hop
5	4	oveq2i	⊢ ( 𝑇 +op ( 𝑈 −op 𝑈 ) ) = ( 𝑇 +op 0hop )
6	1	hoaddid1i	⊢ ( 𝑇 +op 0hop ) = 𝑇
7	3 5 6	3eqtri	⊢ ( ( 𝑇 +op 𝑈 ) −op 𝑈 ) = 𝑇