Metamath Proof Explorer

Theorem hoadd32

Description: Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hoaddcom 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) = ( T +op S ) )
2 1 3adant1 
 |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) = ( T +op S ) )
3 2 oveq2d 
 |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( R +op ( S +op T ) ) = ( R +op ( T +op S ) ) )
4 hoaddass 
 |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( R +op S ) +op T ) = ( R +op ( S +op T ) ) )
5 hoaddass 
 |-  ( ( R : ~H --> ~H /\ T : ~H --> ~H /\ S : ~H --> ~H ) -> ( ( R +op T ) +op S ) = ( R +op ( T +op S ) ) )
6 5 3com23 
 |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( R +op T ) +op S ) = ( R +op ( T +op S ) ) )
7 3 4 6 3eqtr4d 
 |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( R +op S ) +op T ) = ( ( R +op T ) +op S ) )