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

 Description: Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
Assertion
Ref Expression
hoaddsubass ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = (𝑆 +op (𝑇op 𝑈)))

StepHypRef Expression
1 ho0f 28580 . . . 4 0hop : ℋ⟶ ℋ
2 hosubcl 28602 . . . 4 (( 0hop : ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ( 0hopop 𝑈): ℋ⟶ ℋ)
31, 2mpan 705 . . 3 (𝑈: ℋ⟶ ℋ → ( 0hopop 𝑈): ℋ⟶ ℋ)
4 hoaddass 28611 . . 3 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ ( 0hopop 𝑈): ℋ⟶ ℋ) → ((𝑆 +op 𝑇) +op ( 0hopop 𝑈)) = (𝑆 +op (𝑇 +op ( 0hopop 𝑈))))
53, 4syl3an3 1359 . 2 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) +op ( 0hopop 𝑈)) = (𝑆 +op (𝑇 +op ( 0hopop 𝑈))))
6 hoaddcl 28587 . . 3 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇): ℋ⟶ ℋ)
7 ho0sub 28626 . . 3 (((𝑆 +op 𝑇): ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = ((𝑆 +op 𝑇) +op ( 0hopop 𝑈)))
86, 7stoic3 1699 . 2 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = ((𝑆 +op 𝑇) +op ( 0hopop 𝑈)))
9 ho0sub 28626 . . . 4 ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇op 𝑈) = (𝑇 +op ( 0hopop 𝑈)))
1093adant1 1077 . . 3 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇op 𝑈) = (𝑇 +op ( 0hopop 𝑈)))
1110oveq2d 6651 . 2 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 +op (𝑇op 𝑈)) = (𝑆 +op (𝑇 +op ( 0hopop 𝑈))))
125, 8, 113eqtr4d 2664 1 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = (𝑆 +op (𝑇op 𝑈)))