| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > hvmulcl | Structured version Visualization version GIF version | ||
| Description: Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| hvmulcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-hfvmul 31024 | . 2 ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | |
| 2 | 1 | fovcl 7561 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 ℋchba 30938 ·ℎ csm 30940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-hfvmul 31024 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-fv 6569 df-ov 7434 |
| This theorem is referenced by: hvmulcli 31033 hvsubf 31034 hvsubcl 31036 hv2neg 31047 hvaddsubval 31052 hvsub4 31056 hvaddsub12 31057 hvpncan 31058 hvaddsubass 31060 hvsubass 31063 hvsubdistr1 31068 hvsubdistr2 31069 hvaddeq0 31088 hvmulcan 31091 hvmulcan2 31092 hvsubcan 31093 his5 31105 his35 31107 hiassdi 31110 his2sub 31111 hilablo 31179 helch 31262 ocsh 31302 h1de2ci 31575 spansncol 31587 spanunsni 31598 mayete3i 31747 homcl 31765 homulcl 31778 unoplin 31939 hmoplin 31961 bramul 31965 bralnfn 31967 brafnmul 31970 kbop 31972 kbmul 31974 lnopmul 31986 lnopaddmuli 31992 lnopsubmuli 31994 lnopmulsubi 31995 0lnfn 32004 nmlnop0iALT 32014 lnopmi 32019 lnophsi 32020 lnopcoi 32022 lnopeq0i 32026 nmbdoplbi 32043 nmcexi 32045 nmcoplbi 32047 lnfnmuli 32063 lnfnaddmuli 32064 nmbdfnlbi 32068 nmcfnlbi 32071 nlelshi 32079 riesz3i 32081 cnlnadjlem2 32087 cnlnadjlem6 32091 adjlnop 32105 nmopcoi 32114 branmfn 32124 cnvbramul 32134 kbass2 32136 kbass5 32139 superpos 32373 cdj1i 32452 |
| Copyright terms: Public domain | W3C validator |