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

Theorem hosubcl 28478
 Description: Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
Assertion
Ref Expression
hosubcl ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆op 𝑇): ℋ⟶ ℋ)

Proof of Theorem hosubcl
StepHypRef Expression
1 oveq1 6611 . . 3 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → (𝑆op 𝑇) = (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) −op 𝑇))
21feq1d 5987 . 2 (𝑆 = if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) → ((𝑆op 𝑇): ℋ⟶ ℋ ↔ (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) −op 𝑇): ℋ⟶ ℋ))
3 oveq2 6612 . . 3 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) −op 𝑇) = (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) −op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )))
43feq1d 5987 . 2 (𝑇 = if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ) → ((if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) −op 𝑇): ℋ⟶ ℋ ↔ (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) −op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )): ℋ⟶ ℋ))
5 ho0f 28456 . . . 4 0hop : ℋ⟶ ℋ
65elimf 6001 . . 3 if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ): ℋ⟶ ℋ
75elimf 6001 . . 3 if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop ): ℋ⟶ ℋ
86, 7hosubcli 28474 . 2 (if(𝑆: ℋ⟶ ℋ, 𝑆, 0hop ) −op if(𝑇: ℋ⟶ ℋ, 𝑇, 0hop )): ℋ⟶ ℋ
92, 4, 8dedth2h 4112 1 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆op 𝑇): ℋ⟶ ℋ)