Metamath Proof Explorer

Theorem hosub4

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 hosub4 
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) -op ( T +op U ) ) = ( ( R -op T ) +op ( S -op U ) ) )

Proof

Step Hyp Ref Expression
1 honegdi 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T +op U ) ) = ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) )
2 1 adantl 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( -u 1 .op ( T +op U ) ) = ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) )
3 2 oveq2d 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( -u 1 .op ( T +op U ) ) ) = ( ( R +op S ) +op ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) ) )
4 neg1cn 
 |-  -u 1 e. CC
5 homulcl 
 |-  ( ( -u 1 e. CC /\ T : ~H --> ~H ) -> ( -u 1 .op T ) : ~H --> ~H )
6 4 5 mpan 
 |-  ( T : ~H --> ~H -> ( -u 1 .op T ) : ~H --> ~H )
7 homulcl 
 |-  ( ( -u 1 e. CC /\ U : ~H --> ~H ) -> ( -u 1 .op U ) : ~H --> ~H )
8 4 7 mpan 
 |-  ( U : ~H --> ~H -> ( -u 1 .op U ) : ~H --> ~H )
9 6 8 anim12i 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( -u 1 .op T ) : ~H --> ~H /\ ( -u 1 .op U ) : ~H --> ~H ) )
10 hoadd4 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( ( -u 1 .op T ) : ~H --> ~H /\ ( -u 1 .op U ) : ~H --> ~H ) ) -> ( ( R +op S ) +op ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) ) = ( ( R +op ( -u 1 .op T ) ) +op ( S +op ( -u 1 .op U ) ) ) )
11 9 10 sylan2 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) ) = ( ( R +op ( -u 1 .op T ) ) +op ( S +op ( -u 1 .op U ) ) ) )
12 3 11 eqtrd 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( -u 1 .op ( T +op U ) ) ) = ( ( R +op ( -u 1 .op T ) ) +op ( S +op ( -u 1 .op U ) ) ) )
13 hoaddcl 
 |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H ) -> ( R +op S ) : ~H --> ~H )
14 hoaddcl 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op U ) : ~H --> ~H )
15 honegsub 
 |-  ( ( ( R +op S ) : ~H --> ~H /\ ( T +op U ) : ~H --> ~H ) -> ( ( R +op S ) +op ( -u 1 .op ( T +op U ) ) ) = ( ( R +op S ) -op ( T +op U ) ) )
16 13 14 15 syl2an 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( -u 1 .op ( T +op U ) ) ) = ( ( R +op S ) -op ( T +op U ) ) )
17 honegsub 
 |-  ( ( R : ~H --> ~H /\ T : ~H --> ~H ) -> ( R +op ( -u 1 .op T ) ) = ( R -op T ) )
18 17 ad2ant2r 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( R +op ( -u 1 .op T ) ) = ( R -op T ) )
19 honegsub 
 |-  ( ( S : ~H --> ~H /\ U : ~H --> ~H ) -> ( S +op ( -u 1 .op U ) ) = ( S -op U ) )
20 19 ad2ant2l 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( S +op ( -u 1 .op U ) ) = ( S -op U ) )
21 18 20 oveq12d 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op ( -u 1 .op T ) ) +op ( S +op ( -u 1 .op U ) ) ) = ( ( R -op T ) +op ( S -op U ) ) )
22 12 16 21 3eqtr3d 
 |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) -op ( T +op U ) ) = ( ( R -op T ) +op ( S -op U ) ) )