Metamath Proof Explorer

Theorem hoaddsubass

Description: Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoaddsubass 
|- ( ( 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 ho0f 
 |-  0hop : ~H --> ~H
2 hosubcl 
 |-  ( ( 0hop : ~H --> ~H /\ U : ~H --> ~H ) -> ( 0hop -op U ) : ~H --> ~H )
3 1 2 mpan 
 |-  ( U : ~H --> ~H -> ( 0hop -op U ) : ~H --> ~H )
4 hoaddass 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ ( 0hop -op U ) : ~H --> ~H ) -> ( ( S +op T ) +op ( 0hop -op U ) ) = ( S +op ( T +op ( 0hop -op U ) ) ) )
5 3 4 syl3an3 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) +op ( 0hop -op U ) ) = ( S +op ( T +op ( 0hop -op U ) ) ) )
6 hoaddcl 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) : ~H --> ~H )
7 ho0sub 
 |-  ( ( ( S +op T ) : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( S +op T ) +op ( 0hop -op U ) ) )
8 6 7 stoic3 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( S +op T ) +op ( 0hop -op U ) ) )
9 ho0sub 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T -op U ) = ( T +op ( 0hop -op U ) ) )
10 9 3adant1 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T -op U ) = ( T +op ( 0hop -op U ) ) )
11 10 oveq2d 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S +op ( T -op U ) ) = ( S +op ( T +op ( 0hop -op U ) ) ) )
12 5 8 11 3eqtr4d 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( S +op ( T -op U ) ) )