Theorem honpcani

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

	Ref	Expression
Hypotheses	hosd1.2	|- T : ~H --> ~H
	hosd1.3	|- U : ~H --> ~H
Assertion	honpcani	|- ( ( 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	hoaddsubi	|- ( ( T +op U ) -op U ) = ( ( T -op U ) +op U )
4	1 2	hopncani	|- ( ( T +op U ) -op U ) = T
5	3 4	eqtr3i	|- ( ( T -op U ) +op U ) = T