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

Theorem hocofi 30882
Description: Mapping of composition of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
Hypotheses
Ref Expression
hoeq.1 𝑆: ℋ⟶ ℋ
hoeq.2 𝑇: ℋ⟶ ℋ
Assertion
Ref Expression
hocofi (𝑆𝑇): ℋ⟶ ℋ

Proof of Theorem hocofi
StepHypRef Expression
1 hoeq.1 . 2 𝑆: ℋ⟶ ℋ
2 hoeq.2 . 2 𝑇: ℋ⟶ ℋ
3 fco 6728 . 2 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆𝑇): ℋ⟶ ℋ)
41, 2, 3mp2an 690 1 (𝑆𝑇): ℋ⟶ ℋ
Colors of variables: wff setvar class
Syntax hints:  ccom 5673  wf 6528  chba 30035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-fun 6534  df-fn 6535  df-f 6536
This theorem is referenced by:  hocofni  30883  hocadddiri  30895  hocsubdiri  30896  ho2coi  30897  ho0coi  30904  hoid1i  30905  hoid1ri  30906  hoddii  31105  lnopcoi  31119  bdopcoi  31214  adjcoi  31216  nmopcoadji  31217  unierri  31220  pjsdii  31271  pjddii  31272  pjsdi2i  31273  pjss1coi  31279  pjss2coi  31280  pjorthcoi  31285  pjinvari  31307  pjclem1  31311  pjclem4  31315  pjadj2coi  31320  pj3lem1  31322  pj3si  31323  pj3cor1i  31325
  Copyright terms: Public domain W3C validator