![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > lnopfi | Structured version Visualization version GIF version |
Description: A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
Ref | Expression |
---|---|
lnopl.1 | ⊢ 𝑇 ∈ LinOp |
Ref | Expression |
---|---|
lnopfi | ⊢ 𝑇: ℋ⟶ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lnopl.1 | . 2 ⊢ 𝑇 ∈ LinOp | |
2 | lnopf 29290 | . 2 ⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑇: ℋ⟶ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ⟶wf 6131 ℋchba 28348 LinOpclo 28376 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-hilex 28428 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-fv 6143 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-map 8142 df-lnop 29272 |
This theorem is referenced by: lnopaddi 29402 lnopsubi 29405 hoddii 29420 nmlnop0iALT 29426 nmlnopgt0i 29428 lnopmi 29431 lnophsi 29432 lnophdi 29433 lnopcoi 29434 lnopco0i 29435 lnopeq0lem1 29436 lnopeq0i 29438 lnopeqi 29439 lnopunilem1 29441 lnopunilem2 29442 lnophmlem2 29448 lnophmi 29449 nmbdoplbi 29455 nmcopexi 29458 nmcoplbi 29459 lnopconi 29465 imaelshi 29489 rnelshi 29490 cnlnadjlem2 29499 cnlnadjlem6 29503 cnlnadjlem7 29504 cnlnadjeui 29508 nmopcoi 29526 bdopcoi 29529 hmopidmchi 29582 hmopidmpji 29583 |
Copyright terms: Public domain | W3C validator |