Theorem hvaddcl 30941

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 30929	. 2 ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
2	1	fovcl 7517	1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7387   ℋchba 30848   +_ℎ cva 30849

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-hfvadd 30929

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390

This theorem is referenced by:  hvsubf  30944  hvsubcl  30946  hvaddcli  30947  hvadd4  30965  hvsub4  30966  hvpncan  30968  hvaddsubass  30970  hvsubass  30973  hv2times  30990  hvaddsub4  31007  his7  31019  normpyc  31075  hhph  31107  hlimadd  31122  helch  31172  ocsh  31212  spanunsni  31508  3oalem1  31591  pjcompi  31601  mayete3i  31657  hoscl  31674  hoaddcl  31687  unoplin  31849  hmoplin  31871  braadd  31874  0lnfn  31914  lnopmi  31929  lnophsi  31930  lnopcoi  31932  lnopeq0i  31936  nlelshi  31989  cnlnadjlem2  31997  cnlnadjlem6  32001  adjlnop  32015  superpos  32283  cdj3lem2b  32366  cdj3i  32370