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 29390 | . 2 ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | |
2 | 1 | fovcl 7422 | 1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2101 (class class class)co 7295 ℋchba 29309 +ℎ cva 29310 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-sep 5226 ax-nul 5233 ax-pr 5355 ax-hfvadd 29390 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3224 df-v 3436 df-sbc 3719 df-csb 3835 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4260 df-if 4463 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4842 df-iun 4929 df-br 5078 df-opab 5140 df-mpt 5161 df-id 5491 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-iota 6399 df-fun 6449 df-fn 6450 df-f 6451 df-fv 6455 df-ov 7298 |
This theorem is referenced by: hvsubf 29405 hvsubcl 29407 hvaddcli 29408 hvadd4 29426 hvsub4 29427 hvpncan 29429 hvaddsubass 29431 hvsubass 29434 hv2times 29451 hvaddsub4 29468 his7 29480 normpyc 29536 hhph 29568 hlimadd 29583 helch 29633 ocsh 29673 spanunsni 29969 3oalem1 30052 pjcompi 30062 mayete3i 30118 hoscl 30135 hoaddcl 30148 unoplin 30310 hmoplin 30332 braadd 30335 0lnfn 30375 lnopmi 30390 lnophsi 30391 lnopcoi 30393 lnopeq0i 30397 nlelshi 30450 cnlnadjlem2 30458 cnlnadjlem6 30462 adjlnop 30476 superpos 30744 cdj3lem2b 30827 cdj3i 30831 |
Copyright terms: Public domain | W3C validator |