This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem honpcani

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

Step	Hyp	Ref	Expression
1		hosd1.2	$⊢ T : ℋ ⟶ ℋ$
2		hosd1.3	$⊢ U : ℋ ⟶ ℋ$
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$