Theorem hvaddcl 29362

Description: Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)

Assertion

Ref	Expression
hvaddcl	⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ)

Proof of Theorem hvaddcl

Step	Hyp	Ref	Expression
1		ax-hfvadd 29350	. 2 ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
2	1	fovcl 7394	1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2110  (class class class)co 7269   ℋchba 29269   +_ℎ cva 29270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-hfvadd 29350

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-fv 6439  df-ov 7272

This theorem is referenced by:  hvsubf  29365  hvsubcl  29367  hvaddcli  29368  hvadd4  29386  hvsub4  29387  hvpncan  29389  hvaddsubass  29391  hvsubass  29394  hv2times  29411  hvaddsub4  29428  his7  29440  normpyc  29496  hhph  29528  hlimadd  29543  helch  29593  ocsh  29633  spanunsni  29929  3oalem1  30012  pjcompi  30022  mayete3i  30078  hoscl  30095  hoaddcl  30108  unoplin  30270  hmoplin  30292  braadd  30295  0lnfn  30335  lnopmi  30350  lnophsi  30351  lnopcoi  30353  lnopeq0i  30357  nlelshi  30410  cnlnadjlem2  30418  cnlnadjlem6  30422  adjlnop  30436  superpos  30704  cdj3lem2b  30787  cdj3i  30791