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 30207 | . 2 ⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑇: ℋ⟶ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ⟶wf 6423 ℋchba 29267 LinOpclo 29295 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-sep 5222 ax-nul 5229 ax-pow 5287 ax-pr 5351 ax-un 7579 ax-hilex 29347 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3432 df-sbc 3717 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5075 df-opab 5137 df-id 5485 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-iota 6385 df-fun 6429 df-fn 6430 df-f 6431 df-fv 6435 df-ov 7271 df-oprab 7272 df-mpo 7273 df-map 8605 df-lnop 30189 |
This theorem is referenced by: lnopaddi 30319 lnopsubi 30322 hoddii 30337 nmlnop0iALT 30343 nmlnopgt0i 30345 lnopmi 30348 lnophsi 30349 lnophdi 30350 lnopcoi 30351 lnopco0i 30352 lnopeq0lem1 30353 lnopeq0i 30355 lnopeqi 30356 lnopunilem1 30358 lnopunilem2 30359 lnophmlem2 30365 lnophmi 30366 nmbdoplbi 30372 nmcopexi 30375 nmcoplbi 30376 lnopconi 30382 imaelshi 30406 rnelshi 30407 cnlnadjlem2 30416 cnlnadjlem6 30420 cnlnadjlem7 30421 cnlnadjeui 30425 nmopcoi 30443 bdopcoi 30446 hmopidmchi 30499 hmopidmpji 30500 |
Copyright terms: Public domain | W3C validator |