![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > hvaddcl | Structured version Visualization version GIF version |
Description: Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hvaddcl | ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-hfvadd 30882 | . 2 ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | |
2 | 1 | fovcl 7549 | 1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 (class class class)co 7419 ℋchba 30801 +ℎ cva 30802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 ax-hfvadd 30882 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-fv 6557 df-ov 7422 |
This theorem is referenced by: hvsubf 30897 hvsubcl 30899 hvaddcli 30900 hvadd4 30918 hvsub4 30919 hvpncan 30921 hvaddsubass 30923 hvsubass 30926 hv2times 30943 hvaddsub4 30960 his7 30972 normpyc 31028 hhph 31060 hlimadd 31075 helch 31125 ocsh 31165 spanunsni 31461 3oalem1 31544 pjcompi 31554 mayete3i 31610 hoscl 31627 hoaddcl 31640 unoplin 31802 hmoplin 31824 braadd 31827 0lnfn 31867 lnopmi 31882 lnophsi 31883 lnopcoi 31885 lnopeq0i 31889 nlelshi 31942 cnlnadjlem2 31950 cnlnadjlem6 31954 adjlnop 31968 superpos 32236 cdj3lem2b 32319 cdj3i 32323 |
Copyright terms: Public domain | W3C validator |