Theorem hopncani

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

	Ref	Expression
Hypotheses	hosd1.2	|- T : ~H --> ~H
	hosd1.3	|- U : ~H --> ~H
Assertion	hopncani	|- ( ( T +op U ) -op U ) = T

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	|- T : ~H --> ~H
2		hosd1.3	|- U : ~H --> ~H
3	1 2 2	hoaddsubassi	|- ( ( T +op U ) -op U ) = ( T +op ( U -op U ) )
4	2	hodidi	|- ( U -op U ) = 0hop
5	4	oveq2i	|- ( T +op ( U -op U ) ) = ( T +op 0hop )
6	1	hoaddid1i	|- ( T +op 0hop ) = T
7	3 5 6	3eqtri	|- ( ( T +op U ) -op U ) = T