Theorem lnopfi 31008

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 30898	. 2 ⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ)
3	1, 2	ax-mp 5	1 ⊢ 𝑇: ℋ⟶ ℋ

Syntax hints:   ∈ wcel 2106  ⟶wf 6512   ℋchba 29958  LinOpclo 29986

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 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692  ax-hilex 30038

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 3419  df-v 3461  df-sbc 3758  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-br 5126  df-opab 5188  df-id 5551  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-fv 6524  df-ov 7380  df-oprab 7381  df-mpo 7382  df-map 8789  df-lnop 30880

This theorem is referenced by:  lnopaddi  31010  lnopsubi  31013  hoddii  31028  nmlnop0iALT  31034  nmlnopgt0i  31036  lnopmi  31039  lnophsi  31040  lnophdi  31041  lnopcoi  31042  lnopco0i  31043  lnopeq0lem1  31044  lnopeq0i  31046  lnopeqi  31047  lnopunilem1  31049  lnopunilem2  31050  lnophmlem2  31056  lnophmi  31057  nmbdoplbi  31063  nmcopexi  31066  nmcoplbi  31067  lnopconi  31073  imaelshi  31097  rnelshi  31098  cnlnadjlem2  31107  cnlnadjlem6  31111  cnlnadjlem7  31112  cnlnadjeui  31116  nmopcoi  31134  bdopcoi  31137  hmopidmchi  31190  hmopidmpji  31191