Description: Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27Jul2006) (New usage is discouraged.)
Ref  Expression  

Hypotheses  hods.1   R : ~H > ~H 

hods.2   S : ~H > ~H 

hods.3   T : ~H > ~H 

Assertion  hoadd32i   ( ( R +op S ) +op T ) = ( ( R +op T ) +op S ) 
Step  Hyp  Ref  Expression 

1  hods.1   R : ~H > ~H 

2  hods.2   S : ~H > ~H 

3  hods.3   T : ~H > ~H 

4  2 3  hoaddcomi   ( S +op T ) = ( T +op S ) 
5  4  oveq2i   ( R +op ( S +op T ) ) = ( R +op ( T +op S ) ) 
6  1 2 3  hoaddassi   ( ( R +op S ) +op T ) = ( R +op ( S +op T ) ) 
7  1 3 2  hoaddassi   ( ( R +op T ) +op S ) = ( R +op ( T +op S ) ) 
8  5 6 7  3eqtr4i   ( ( R +op S ) +op T ) = ( ( R +op T ) +op S ) 