Theorem lnopf 9893

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 9785	. 2 |- (T e. LinOp -> T:H~-->H~)
3	1, 2	ax-mp 7	1 |- T:H~-->H~

Syntax hints:   e. wcel 958  -->wf 3178  H~chil 8788  LinOpclo 8816

This theorem is referenced by:  lnopadd 9895  lnopsub 9898  hoddi 9914  nmlnop0ALT 9920  nmlnopgt0 9922  lnopm 9925  lnophs 9926  lnophd 9927  lnopco 9928  lnopco0 9929  lnopeq0lem1 9930  lnopeq0 9932  lnopeq 9933  lnopunilem1 9935  lnopunilem2 9936  lnophmlem2 9942  lnophm 9943  nmbdoplb 9949  nmcopexlem1 9951  nmcopexlem2 9952  nmcopexlem3 9953  nmcopexlem6 9956  nmcoplb 9958  lnopcon 9963  cnlnadjlem2 10001  cnlnadjlem6 10005  cnlnadjlem7 10006  cnlnadjeu 10010  nmopco 10028  bdopco 10031  hmopidmchlem 10078  hmopidmch 10079  hmopidmpj 10080

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-hilex 8869

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-fv 3198  df-opr 3965  df-lnop 9767

Copyright terms: Public domain