Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  hoaddcom Structured version   Visualization version   GIF version

 Description: Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
Assertion
Ref Expression
hoaddcom ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇) = (𝑇 +op 𝑆))

StepHypRef Expression
1 oveq1 6820 . . 3 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → (𝑆 +op 𝑇) = (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇))
2 oveq2 6821 . . 3 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → (𝑇 +op 𝑆) = (𝑇 +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )))
31, 2eqeq12d 2775 . 2 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → ((𝑆 +op 𝑇) = (𝑇 +op 𝑆) ↔ (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇) = (𝑇 +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ))))
4 oveq2 6821 . . 3 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇) = (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )))
5 oveq1 6820 . . 3 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → (𝑇 +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) = (if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )))
64, 5eqeq12d 2775 . 2 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → ((if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇) = (𝑇 +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) ↔ (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )) = (if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ))))
7 ho0f 28919 . . . 4 0hop : ℋ⟶ ℋ
87elimf 6205 . . 3 if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ): ℋ⟶ ℋ
97elimf 6205 . . 3 if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ): ℋ⟶ ℋ
108, 9hoaddcomi 28940 . 2 (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )) = (if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ))
113, 6, 10dedth2h 4284 1 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇) = (𝑇 +op 𝑆))