Metamath Proof Explorer

Theorem hosubsub2

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

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

Proof

Step Hyp Ref Expression
1 hosubcl 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T -op U ) : ~H --> ~H )
2 honegsub 
 |-  ( ( S : ~H --> ~H /\ ( T -op U ) : ~H --> ~H ) -> ( S +op ( -u 1 .op ( T -op U ) ) ) = ( S -op ( T -op U ) ) )
3 1 2 sylan2 
 |-  ( ( S : ~H --> ~H /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( S +op ( -u 1 .op ( T -op U ) ) ) = ( S -op ( T -op U ) ) )
4 3 3impb 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S +op ( -u 1 .op ( T -op U ) ) ) = ( S -op ( T -op U ) ) )
5 honegsubdi2 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T -op U ) ) = ( U -op T ) )
6 5 oveq2d 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S +op ( -u 1 .op ( T -op U ) ) ) = ( S +op ( U -op T ) ) )
7 6 3adant1 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S +op ( -u 1 .op ( T -op U ) ) ) = ( S +op ( U -op T ) ) )
8 4 7 eqtr3d 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op ( T -op U ) ) = ( S +op ( U -op T ) ) )