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

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

StepHypRef Expression
1 oveq1 6799 . . . 4 (𝑅 = if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) → (𝑅 +op 𝑆) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op 𝑆))
21oveq1d 6807 . . 3 (𝑅 = if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) → ((𝑅 +op 𝑆) +op 𝑇) = ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op 𝑆) +op 𝑇))
3 oveq1 6799 . . 3 (𝑅 = if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) → (𝑅 +op (𝑆 +op 𝑇)) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (𝑆 +op 𝑇)))
42, 3eqeq12d 2785 . 2 (𝑅 = if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) → (((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇)) ↔ ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op 𝑆) +op 𝑇) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (𝑆 +op 𝑇))))
5 oveq2 6800 . . . 4 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op 𝑆) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )))
65oveq1d 6807 . . 3 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op 𝑆) +op 𝑇) = ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) +op 𝑇))
7 oveq1 6799 . . . 4 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → (𝑆 +op 𝑇) = (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇))
87oveq2d 6808 . . 3 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (𝑆 +op 𝑇)) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇)))
96, 8eqeq12d 2785 . 2 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → (((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op 𝑆) +op 𝑇) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (𝑆 +op 𝑇)) ↔ ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) +op 𝑇) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇))))
10 oveq2 6800 . . 3 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) +op 𝑇) = ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )))
11 oveq2 6800 . . . 4 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇) = (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )))
1211oveq2d 6808 . . 3 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇)) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ))))
1310, 12eqeq12d 2785 . 2 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → (((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) +op 𝑇) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op 𝑇)) ↔ ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )))))
14 ho0f 28944 . . . 4 0hop : ℋ⟶ ℋ
1514elimf 6184 . . 3 if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ): ℋ⟶ ℋ
1614elimf 6184 . . 3 if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ): ℋ⟶ ℋ
1714elimf 6184 . . 3 if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ): ℋ⟶ ℋ
1815, 16, 17hoaddassi 28969 . 2 ((if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop )) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )) = (if(𝑅: ℋ⟶ ℋ, 𝑅, 0hop ) +op (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) +op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )))
194, 9, 13, 18dedth3h 4278 1 ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇)))