Metamath Proof Explorer

Theorem hosubsub

Description: Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hosubsub 
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op ( T -op U ) ) = ( ( S -op T ) +op U ) )

Proof

Step Hyp Ref Expression
1 hosubsub2 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op ( T -op U ) ) = ( S +op ( U -op T ) ) )
2 hoaddsubass 
 |-  ( ( S : ~H --> ~H /\ U : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( S +op U ) -op T ) = ( S +op ( U -op T ) ) )
3 hoaddsub 
 |-  ( ( S : ~H --> ~H /\ U : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( S +op U ) -op T ) = ( ( S -op T ) +op U ) )
4 2 3 eqtr3d 
 |-  ( ( S : ~H --> ~H /\ U : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op ( U -op T ) ) = ( ( S -op T ) +op U ) )
5 4 3com23 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S +op ( U -op T ) ) = ( ( S -op T ) +op U ) )
6 1 5 eqtrd 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op ( T -op U ) ) = ( ( S -op T ) +op U ) )