![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > hocoi | Structured version Visualization version GIF version |
Description: Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hoeq.1 | ⊢ 𝑆: ℋ⟶ ℋ |
hoeq.2 | ⊢ 𝑇: ℋ⟶ ℋ |
Ref | Expression |
---|---|
hocoi | ⊢ (𝐴 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝐴) = (𝑆‘(𝑇‘𝐴))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hoeq.2 | . 2 ⊢ 𝑇: ℋ⟶ ℋ | |
2 | fvco3 6588 | . 2 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑆 ∘ 𝑇)‘𝐴) = (𝑆‘(𝑇‘𝐴))) | |
3 | 1, 2 | mpan 677 | 1 ⊢ (𝐴 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝐴) = (𝑆‘(𝑇‘𝐴))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 ∘ ccom 5411 ⟶wf 6184 ‘cfv 6188 ℋchba 28475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ne 2969 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3418 df-sbc 3683 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-id 5312 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-fv 6196 |
This theorem is referenced by: hococli 29323 hocadddiri 29337 hocsubdiri 29338 ho2coi 29339 ho0coi 29346 hoid1i 29347 hoid1ri 29348 hoddii 29547 lnopcoi 29561 lnopco0i 29562 nmopcoi 29653 adjcoi 29658 nmopcoadji 29659 hmopidmchi 29709 hmopidmpji 29710 pjsdii 29713 pjddii 29714 pjcoi 29716 pjcohocli 29761 pjadj2coi 29762 pj3lem1 29764 |
Copyright terms: Public domain | W3C validator |