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	$$⊢{+}_{ℎ}:\mathscr{H}\times \mathscr{H}⟶\mathscr{H}$$

Detailed syntax breakdown

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