# Metamath Proof Explorer

Description: Rearrangement of 4 terms in a sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
`|- ( ( ( 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
` |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( R +op S ) +op T ) = ( ( R +op T ) +op S ) )`
2 1 oveq1d
` |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( ( R +op S ) +op T ) +op U ) = ( ( ( R +op T ) +op S ) +op U ) )`
3 2 3expa
` |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ T : ~H --> ~H ) -> ( ( ( R +op S ) +op T ) +op U ) = ( ( ( R +op T ) +op S ) +op U ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H ) -> ( R +op S ) : ~H --> ~H )`
` |-  ( ( ( R +op S ) : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( ( R +op S ) +op T ) +op U ) = ( ( R +op S ) +op ( T +op U ) ) )`
7 6 3expb
` |-  ( ( ( R +op S ) : ~H --> ~H /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( ( R +op S ) +op T ) +op U ) = ( ( R +op S ) +op ( T +op U ) ) )`
8 5 7 sylan
` |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( ( R +op S ) +op T ) +op U ) = ( ( R +op S ) +op ( T +op U ) ) )`
` |-  ( ( R : ~H --> ~H /\ T : ~H --> ~H ) -> ( R +op T ) : ~H --> ~H )`
` |-  ( ( ( R +op T ) : ~H --> ~H /\ S : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( ( R +op T ) +op S ) +op U ) = ( ( R +op T ) +op ( S +op U ) ) )`
` |-  ( ( ( R +op T ) : ~H --> ~H /\ ( S : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( ( R +op T ) +op S ) +op U ) = ( ( R +op T ) +op ( S +op U ) ) )`
` |-  ( ( ( R : ~H --> ~H /\ T : ~H --> ~H ) /\ ( S : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( ( R +op T ) +op S ) +op U ) = ( ( R +op T ) +op ( S +op U ) ) )`
` |-  ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( ( R +op T ) +op S ) +op U ) = ( ( R +op T ) +op ( S +op U ) ) )`
` |-  ( ( ( 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 ) ) )`