Description: Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hods.1 | ⊢ 𝑅 : ℋ ⟶ ℋ | |
| hods.2 | ⊢ 𝑆 : ℋ ⟶ ℋ | ||
| hods.3 | ⊢ 𝑇 : ℋ ⟶ ℋ | ||
| Assertion | hoadd32i | ⊢ ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( ( 𝑅 +op 𝑇 ) +op 𝑆 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hods.1 | ⊢ 𝑅 : ℋ ⟶ ℋ | |
| 2 | hods.2 | ⊢ 𝑆 : ℋ ⟶ ℋ | |
| 3 | hods.3 | ⊢ 𝑇 : ℋ ⟶ ℋ | |
| 4 | 2 3 | hoaddcomi | ⊢ ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 ) |
| 5 | 4 | oveq2i | ⊢ ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) = ( 𝑅 +op ( 𝑇 +op 𝑆 ) ) |
| 6 | 1 2 3 | hoaddassi | ⊢ ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) |
| 7 | 1 3 2 | hoaddassi | ⊢ ( ( 𝑅 +op 𝑇 ) +op 𝑆 ) = ( 𝑅 +op ( 𝑇 +op 𝑆 ) ) |
| 8 | 5 6 7 | 3eqtr4i | ⊢ ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( ( 𝑅 +op 𝑇 ) +op 𝑆 ) |