Theorem honpncani

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

	Ref	Expression
Hypotheses	honpncan.1	|- R : ~H --> ~H
	honpncan.2	|- S : ~H --> ~H
	honpncan.3	|- T : ~H --> ~H
Assertion	honpncani	|- ( ( R -op S ) +op ( S -op T ) ) = ( R -op T )

Proof

Step	Hyp	Ref	Expression
1		honpncan.1	|- R : ~H --> ~H
2		honpncan.2	|- S : ~H --> ~H
3		honpncan.3	|- T : ~H --> ~H
4	1 2	hosubcli	|- ( R -op S ) : ~H --> ~H
5	4 2 3	hoaddsubassi	|- ( ( ( R -op S ) +op S ) -op T ) = ( ( R -op S ) +op ( S -op T ) )
6	1 2	honpcani	|- ( ( R -op S ) +op S ) = R
7	6	oveq1i	|- ( ( ( R -op S ) +op S ) -op T ) = ( R -op T )
8	5 7	eqtr3i	|- ( ( R -op S ) +op ( S -op T ) ) = ( R -op T )