Theorem hvaddcl 31607

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7418   ℋchba 31514   +_ℎ cva 31515

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-hfvadd 31595

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7421

This theorem is used by:  hvsubf  31610  hvsubcl  31612  hvaddcli  31613  hvadd4  31631  hvsub4  31632  hvpncan  31634  hvaddsubass  31636  hvsubass  31639  hv2times  31656  hvaddsub4  31673  his7  31685  normpyc  31741  hhph  31773  hlimadd  31788  helch  31838  ocsh  31878  spanunsni  32174  3oalem1  32257  pjcompi  32267  mayete3i  32323  hoscl  32340  hoaddcl  32353  unoplin  32515  hmoplin  32537  braadd  32540  0lnfn  32580  lnopmi  32595  lnophsi  32596  lnopcoi  32598  lnopeq0i  32602  nlelshi  32655  cnlnadjlem2  32663  cnlnadjlem6  32667  adjlnop  32681  superpos  32949  cdj3lem2b  33032  cdj3i  33036