Axiom ax-hvaddcl 4984

Description: Closure of vector addition.

Assertion

Ref	Expression
ax-hvaddcl	|- ((A e. H~ /\ B e. H~) -> (A +v B) e. H~)

Detailed syntax breakdown of Axiom ax-hvaddcl

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 4958	. . . 4 class H~
3	1, 2	wcel 1092	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 1092	. . 3 wff B e. H~
6	3, 5	wa 196	. 2 wff (A e. H~ /\ B e. H~)
7		cva 4959	. . . 4 class +v
8	1, 4, 7	co 3001	. . 3 class (A +v B)
9	8, 2	wcel 1092	. 2 wff (A +v B) e. H~
10	6, 9	wi 2	1 wff ((A e. H~ /\ B e. H~) -> (A +v B) e. H~)

This axiom is referenced by:  hvsubclt 4998  hvaddcl 4999  hvadd4t 5013  hvsub4t 5014  hvsubcan1t 5016  hvaddsubasst 5018  his7 5051  normpyct 5093  helch 5151  ocsh 5164  shselt 5280  spanunsn 5482  hosclt 5491  osumlem1 5530  3oalem1 5552  hosf 5602

metamath.org