Axiom ax-hvass

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

	Ref	Expression
Assertion	ax-hvass	|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h B ) +h C ) = ( A +h ( B +h C ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		chba	|- ~H
2	0 1	wcel	|- A e. ~H
3		cB	|- B
4	3 1	wcel	|- B e. ~H
5		cC	|- C
6	5 1	wcel	|- C e. ~H
7	2 4 6	w3a	|- ( A e. ~H /\ B e. ~H /\ C e. ~H )
8		cva	|- +h
9	0 3 8	co	|- ( A +h B )
10	9 5 8	co	|- ( ( A +h B ) +h C )
11	3 5 8	co	|- ( B +h C )
12	0 11 8	co	|- ( A +h ( B +h C ) )
13	10 12	wceq	|- ( ( A +h B ) +h C ) = ( A +h ( B +h C ) )
14	7 13	wi	|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h B ) +h C ) = ( A +h ( B +h C ) ) )