Description: Commutative/associative law for Hilbert space operator sum that swaps the first two terms. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hods.1 | ⊢ 𝑅 : ℋ ⟶ ℋ | |
| hods.2 | ⊢ 𝑆 : ℋ ⟶ ℋ | ||
| hods.3 | ⊢ 𝑇 : ℋ ⟶ ℋ | ||
| Assertion | hoadd12i | ⊢ ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) = ( 𝑆 +op ( 𝑅 +op 𝑇 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hods.1 | ⊢ 𝑅 : ℋ ⟶ ℋ | |
| 2 | hods.2 | ⊢ 𝑆 : ℋ ⟶ ℋ | |
| 3 | hods.3 | ⊢ 𝑇 : ℋ ⟶ ℋ | |
| 4 | 1 2 | hoaddcomi | ⊢ ( 𝑅 +op 𝑆 ) = ( 𝑆 +op 𝑅 ) |
| 5 | 4 | oveq1i | ⊢ ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( ( 𝑆 +op 𝑅 ) +op 𝑇 ) |
| 6 | 1 2 3 | hoaddassi | ⊢ ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) |
| 7 | 2 1 3 | hoaddassi | ⊢ ( ( 𝑆 +op 𝑅 ) +op 𝑇 ) = ( 𝑆 +op ( 𝑅 +op 𝑇 ) ) |
| 8 | 5 6 7 | 3eqtr3i | ⊢ ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) = ( 𝑆 +op ( 𝑅 +op 𝑇 ) ) |