ax-hvass

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

		Ref	Expression
	Assertion	ax-hvass	$⊢ (A \in ℋ \land B \in ℋ \land C \in ℋ) \to (A +_{ℎ} B) +_{ℎ} C = A +_{ℎ} (B +_{ℎ} C)$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		chba	$class ℋ$
2	0 1	wcel	$wff A \in ℋ$
3		cB	$class B$
4	3 1	wcel	$wff B \in ℋ$
5		cC	$class C$
6	5 1	wcel	$wff C \in ℋ$
7	2 4 6	w3a	$wff (A \in ℋ \land B \in ℋ \land C \in ℋ)$
8		cva	$class +_{ℎ}$
9	0 3 8	co	$class (A +_{ℎ} B)$
10	9 5 8	co	$class ((A +_{ℎ} B) +_{ℎ} C)$
11	3 5 8	co	$class (B +_{ℎ} C)$
12	0 11 8	co	$class (A +_{ℎ} (B +_{ℎ} C))$
13	10 12	wceq	$wff (A +_{ℎ} B) +_{ℎ} C = A +_{ℎ} (B +_{ℎ} C)$
14	7 13	wi	$wff ((A \in ℋ \land B \in ℋ \land C \in ℋ) \to (A +_{ℎ} B) +_{ℎ} C = A +_{ℎ} (B +_{ℎ} C))$

Metamath Proof Explorer