Metamath Proof Explorer

Theorem hoaddsub

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

Ref Expression
Assertion hoaddsub 
|- ( ( 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 hoaddcom 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) = ( T +op S ) )
2 1 oveq1d 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( T +op S ) -op U ) )
3 2 3adant3 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( T +op S ) -op U ) )
4 hoaddsubass 
 |-  ( ( T : ~H --> ~H /\ S : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( T +op S ) -op U ) = ( T +op ( S -op U ) ) )
5 4 3com12 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( T +op S ) -op U ) = ( T +op ( S -op U ) ) )
6 hosubcl 
 |-  ( ( S : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op U ) : ~H --> ~H )
7 hoaddcom 
 |-  ( ( T : ~H --> ~H /\ ( S -op U ) : ~H --> ~H ) -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) )
8 7 ex 
 |-  ( T : ~H --> ~H -> ( ( S -op U ) : ~H --> ~H -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) )
9 6 8 syl5 
 |-  ( T : ~H --> ~H -> ( ( S : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) )
10 9 expd 
 |-  ( T : ~H --> ~H -> ( S : ~H --> ~H -> ( U : ~H --> ~H -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) ) )
11 10 com12 
 |-  ( S : ~H --> ~H -> ( T : ~H --> ~H -> ( U : ~H --> ~H -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) ) )
12 11 3imp 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) )
13 3 5 12 3eqtrd 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( S -op U ) +op T ) )