Axiom ax-hvcom

Description: Vector addition is commutative. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hvcom	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{+}_{ℎ}B=B{+}_{ℎ}A$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		chba	$$class\mathscr{H}$$
2	0 1	wcel	$$wffA\in \mathscr{H}$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in \mathscr{H}$$
5	2 4	wa	$$wff\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)$$
6		cva	$$class{+}_{ℎ}$$
7	0 3 6	co	$$class\left(A{+}_{ℎ}B\right)$$
8	3 0 6	co	$$class\left(B{+}_{ℎ}A\right)$$
9	7 8	wceq	$$wffA{+}_{ℎ}B=B{+}_{ℎ}A$$
10	5 9	wi	$$wff\left(\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{+}_{ℎ}B=B{+}_{ℎ}A\right)$$