Theorem lnopfi 32059

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	⊢ 𝑇 ∈ LinOp

Assertion

Ref	Expression
lnopfi	⊢ 𝑇: ℋ⟶ ℋ

Proof of Theorem lnopfi

Step	Hyp	Ref	Expression
1		lnopl.1	. 2 ⊢ 𝑇 ∈ LinOp
2		lnopf 31949	. 2 ⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ)
3	1, 2	ax-mp 5	1 ⊢ 𝑇: ℋ⟶ ℋ

Syntax hints:   ∈ wcel 2114  ⟶wf 6490   ℋchba 31009  LinOpclo 31037

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-hilex 31089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-fv 6502  df-ov 7365  df-oprab 7366  df-mpo 7367  df-map 8770  df-lnop 31931

This theorem is referenced by:  lnopaddi  32061  lnopsubi  32064  hoddii  32079  nmlnop0iALT  32085  nmlnopgt0i  32087  lnopmi  32090  lnophsi  32091  lnophdi  32092  lnopcoi  32093  lnopco0i  32094  lnopeq0lem1  32095  lnopeq0i  32097  lnopeqi  32098  lnopunilem1  32100  lnopunilem2  32101  lnophmlem2  32107  lnophmi  32108  nmbdoplbi  32114  nmcopexi  32117  nmcoplbi  32118  lnopconi  32124  imaelshi  32148  rnelshi  32149  cnlnadjlem2  32158  cnlnadjlem6  32162  cnlnadjlem7  32163  cnlnadjeui  32167  nmopcoi  32185  bdopcoi  32188  hmopidmchi  32241  hmopidmpji  32242