![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > homulcl | Structured version Visualization version GIF version |
Description: The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Ref | Expression |
---|---|
homulcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op 𝑇): ℋ⟶ ℋ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffvelrn 6705 | . . . . 5 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ) | |
2 | hvmulcl 28469 | . . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → (𝐴 ·ℎ (𝑇‘𝑥)) ∈ ℋ) | |
3 | 1, 2 | sylan2 592 | . . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ)) → (𝐴 ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
4 | 3 | anassrs 468 | . . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (𝐴 ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
5 | 4 | fmpttd 6733 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝑥 ∈ ℋ ↦ (𝐴 ·ℎ (𝑇‘𝑥))): ℋ⟶ ℋ) |
6 | hommval 29192 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op 𝑇) = (𝑥 ∈ ℋ ↦ (𝐴 ·ℎ (𝑇‘𝑥)))) | |
7 | 6 | feq1d 6359 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 ·op 𝑇): ℋ⟶ ℋ ↔ (𝑥 ∈ ℋ ↦ (𝐴 ·ℎ (𝑇‘𝑥))): ℋ⟶ ℋ)) |
8 | 5, 7 | mpbird 258 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op 𝑇): ℋ⟶ ℋ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2079 ↦ cmpt 5035 ⟶wf 6213 ‘cfv 6217 (class class class)co 7007 ℂcc 10370 ℋchba 28375 ·ℎ csm 28377 ·op chot 28395 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-rep 5075 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-hilex 28455 ax-hfvmul 28461 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-ral 3108 df-rex 3109 df-reu 3110 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-iun 4821 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-ov 7010 df-oprab 7011 df-mpo 7012 df-map 8249 df-homul 29187 |
This theorem is referenced by: honegsubi 29252 homulid2 29256 homco1 29257 homulass 29258 hoadddi 29259 hoadddir 29260 hosubneg 29263 hosubdi 29264 honegsubdi 29266 honegsubdi2 29267 hosub4 29269 hosubsub4 29274 hosubeq0i 29282 nmopnegi 29421 homco2 29433 lnopmi 29456 hmopm 29477 nmophmi 29487 adjmul 29548 opsqrlem1 29596 opsqrlem6 29601 |
Copyright terms: Public domain | W3C validator |