Metamath Proof Explorer

Theorem hosubsub4

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

Ref Expression
Assertion hosubsub4 
|- ( ( 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 neg1cn 
 |-  -u 1 e. CC
2 homulcl 
 |-  ( ( -u 1 e. CC /\ U : ~H --> ~H ) -> ( -u 1 .op U ) : ~H --> ~H )
3 1 2 mpan 
 |-  ( U : ~H --> ~H -> ( -u 1 .op U ) : ~H --> ~H )
4 hosubsub 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ ( -u 1 .op U ) : ~H --> ~H ) -> ( S -op ( T -op ( -u 1 .op U ) ) ) = ( ( S -op T ) +op ( -u 1 .op U ) ) )
5 3 4 syl3an3 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op ( T -op ( -u 1 .op U ) ) ) = ( ( S -op T ) +op ( -u 1 .op U ) ) )
6 hosubneg 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T -op ( -u 1 .op U ) ) = ( T +op U ) )
7 6 3adant1 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T -op ( -u 1 .op U ) ) = ( T +op U ) )
8 7 oveq2d 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op ( T -op ( -u 1 .op U ) ) ) = ( S -op ( T +op U ) ) )
9 hosubcl 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) : ~H --> ~H )
10 honegsub 
 |-  ( ( ( S -op T ) : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S -op T ) +op ( -u 1 .op U ) ) = ( ( S -op T ) -op U ) )
11 9 10 stoic3 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S -op T ) +op ( -u 1 .op U ) ) = ( ( S -op T ) -op U ) )
12 5 8 11 3eqtr3rd 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S -op T ) -op U ) = ( S -op ( T +op U ) ) )