Theorem lnopfi 32598

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

This proof depends on syntax axioms:   ∈ wcel 2147  ⟶wf 6551   ℋchba 31548  LinOpclo 31576

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-hilex 31628

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-map 8874  df-lnop 32470

This theorem is used by:  lnopaddi  32600  lnopsubi  32603  hoddii  32618  nmlnop0iALT  32624  nmlnopgt0i  32626  lnopmi  32629  lnophsi  32630  lnophdi  32631  lnopcoi  32632  lnopco0i  32633  lnopeq0lem1  32634  lnopeq0i  32636  lnopeqi  32637  lnopunilem1  32639  lnopunilem2  32640  lnophmlem2  32646  lnophmi  32647  nmbdoplbi  32653  nmcopexi  32656  nmcoplbi  32657  lnopconi  32663  imaelshi  32687  rnelshi  32688  cnlnadjlem2  32697  cnlnadjlem6  32701  cnlnadjlem7  32702  cnlnadjeui  32706  nmopcoi  32724  bdopcoi  32727  hmopidmchi  32780  hmopidmpji  32781