This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Axiom ax-hfvadd

Description: Vector addition is an operation on ~H . (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	ax-hfvadd	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ$

Step	Hyp	Ref	Expression
0		cva	$class +_{ℎ}$
1		chba	$class ℋ$
2	1 1	cxp	$class (ℋ \times ℋ)$
3	2 1 0	wf	$wff +_{ℎ} : ℋ \times ℋ ⟶ ℋ$