HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  lnopfi Structured version   Unicode version

Theorem lnopfi 27287
Description: A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
Hypothesis
Ref Expression
lnopl.1  |-  T  e. 
LinOp
Assertion
Ref Expression
lnopfi  |-  T : ~H
--> ~H

Proof of Theorem lnopfi
StepHypRef Expression
1 lnopl.1 . 2  |-  T  e. 
LinOp
2 lnopf 27177 . 2  |-  ( T  e.  LinOp  ->  T : ~H
--> ~H )
31, 2ax-mp 5 1  |-  T : ~H
--> ~H
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842   -->wf 5564   ~Hchil 26236   LinOpclo 26264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-hilex 26316
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-fv 5576  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-map 7458  df-lnop 27159
This theorem is referenced by:  lnopaddi  27289  lnopsubi  27292  hoddii  27307  nmlnop0iALT  27313  nmlnopgt0i  27315  lnopmi  27318  lnophsi  27319  lnophdi  27320  lnopcoi  27321  lnopco0i  27322  lnopeq0lem1  27323  lnopeq0i  27325  lnopeqi  27326  lnopunilem1  27328  lnopunilem2  27329  lnophmlem2  27335  lnophmi  27336  nmbdoplbi  27342  nmcopexi  27345  nmcoplbi  27346  lnopconi  27352  imaelshi  27376  rnelshi  27377  cnlnadjlem2  27386  cnlnadjlem6  27390  cnlnadjlem7  27391  cnlnadjeui  27395  nmopcoi  27413  bdopcoi  27416  hmopidmchi  27469  hmopidmpji  27470
  Copyright terms: Public domain W3C validator