Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > hoaddcli | Structured version Visualization version GIF version |
Description: Mapping of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hoeq.1 | ⊢ 𝑆: ℋ⟶ ℋ |
hoeq.2 | ⊢ 𝑇: ℋ⟶ ℋ |
Ref | Expression |
---|---|
hoaddcli | ⊢ (𝑆 +op 𝑇): ℋ⟶ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hoeq.1 | . 2 ⊢ 𝑆: ℋ⟶ ℋ | |
2 | hoeq.2 | . 2 ⊢ 𝑇: ℋ⟶ ℋ | |
3 | hoaddcl 29514 | . 2 ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇): ℋ⟶ ℋ) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ (𝑆 +op 𝑇): ℋ⟶ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ⟶wf 6332 (class class class)co 7137 ℋchba 28675 +op chos 28694 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2792 ax-rep 5171 ax-sep 5184 ax-nul 5191 ax-pow 5247 ax-pr 5311 ax-un 7442 ax-hilex 28755 ax-hfvadd 28756 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2653 df-clab 2799 df-cleq 2813 df-clel 2891 df-nfc 2959 df-ne 3012 df-ral 3138 df-rex 3139 df-reu 3140 df-rab 3142 df-v 3483 df-sbc 3759 df-csb 3867 df-dif 3922 df-un 3924 df-in 3926 df-ss 3935 df-nul 4275 df-if 4449 df-pw 4522 df-sn 4549 df-pr 4551 df-op 4555 df-uni 4820 df-iun 4902 df-br 5048 df-opab 5110 df-mpt 5128 df-id 5441 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-iota 6295 df-fun 6338 df-fn 6339 df-f 6340 df-f1 6341 df-fo 6342 df-f1o 6343 df-fv 6344 df-ov 7140 df-oprab 7141 df-mpo 7142 df-map 8389 df-hosum 29486 |
This theorem is referenced by: hoaddfni 29526 hoaddcomi 29528 hodsi 29531 hoaddassi 29532 hocadddiri 29535 hoaddid1i 29542 ho0subi 29551 honegsubi 29552 hosd1i 29578 lnophsi 29757 nmoptrii 29850 bdophsi 29852 nmoptri2i 29855 pjsdii 29911 pjscji 29926 pjtoi 29935 |
Copyright terms: Public domain | W3C validator |