Theorem hoaddsubi

Description: Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

Proof

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