Theorem hoaddsubassi

Description: Associativity of 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	hoaddsubassi	|- ( ( R +op S ) -op T ) = ( R +op ( S -op T ) )

Proof

Step	Hyp	Ref	Expression
1		hoaddsubass.1	|- R : ~H --> ~H
2		hoaddsubass.2	|- S : ~H --> ~H
3		hoaddsubass.3	|- T : ~H --> ~H
4		hoaddsubass	|- ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( R +op S ) -op T ) = ( R +op ( S -op T ) ) )
5	1 2 3 4	mp3an	|- ( ( R +op S ) -op T ) = ( R +op ( S -op T ) )