Metamath Proof Explorer

Theorem hosubadd4

Description: Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hosubcl 
 |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H ) -> ( R -op S ) : ~H --> ~H )
2 hosubsub2 
 |-  ( ( ( R -op S ) : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( R -op S ) -op ( T -op U ) ) = ( ( R -op S ) +op ( U -op T ) ) )
3 2 3expb 
 |-  ( ( ( R -op S ) : ~H --> ~H /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R -op S ) -op ( T -op U ) ) = ( ( R -op S ) +op ( U -op T ) ) )
4 1 3 sylan 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R -op S ) -op ( T -op U ) ) = ( ( R -op S ) +op ( U -op T ) ) )
5 hosub4 
 |-  ( ( ( R : ~H --> ~H /\ U : ~H --> ~H ) /\ ( S : ~H --> ~H /\ T : ~H --> ~H ) ) -> ( ( R +op U ) -op ( S +op T ) ) = ( ( R -op S ) +op ( U -op T ) ) )
6 5 an42s 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op U ) -op ( S +op T ) ) = ( ( R -op S ) +op ( U -op T ) ) )
7 4 6 eqtr4d 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R -op S ) -op ( T -op U ) ) = ( ( R +op U ) -op ( S +op T ) ) )