Theorem lnopf 9809

Description: A linear Hilbert space operator is a Hilbert space operator.

Hypothesis

Ref	Expression
lnopl.1	|- T e. LinOp

Assertion

Ref	Expression
lnopf	|- T:H~-->H~

Proof of Theorem lnopf

Step	Hyp	Ref	Expression
1		lnopl.1	. 2 |- T e. LinOp
2		lnopft 9702	. 2 |- (T e. LinOp -> T:H~-->H~)
3	1, 2	ax-mp 7	1 |- T:H~-->H~

Syntax hints:   e. wcel 955  -->wf 3168  H~chil 8727  LinOpclo 8755

This theorem is referenced by:  lnopadd 9811  lnopsub 9814  hoddi 9829  nmlnop0ALT 9835  nmlnopgt0 9837  lnopm 9840  lnophs 9841  lnophd 9842  lnopco 9843  lnopco0 9844  lnopeq0lem1 9845  lnopeq0 9847  lnopeq 9848  lnopunilem1 9850  lnopunilem2 9851  lnophmlem2 9857  lnophm 9858  nmbdoplb 9864  nmcopexlem1 9866  nmcopexlem2 9867  nmcopexlem3 9868  nmcopexlem6 9871  nmcoplb 9873  lnopcon 9878  cnlnadjlem2 9916  cnlnadjlem6 9920  cnlnadjlem7 9921  cnlnadjeu 9925  nmopco 9942  bdopco 9945  hmopidmchlem 9989  hmopidmch 9990  hmopidmpj 9991

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-hilex 8790

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-fv 3188  df-opr 3950  df-lnop 9684

Copyright terms: Public domain