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

Metamath Proof Explorer

Theorem hvadd12i

Description: Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		hvass.1	$⊢ A \in ℋ$
2		hvass.2	$⊢ B \in ℋ$
3		hvass.3	$⊢ C \in ℋ$
4	1 2	hvcomi	$⊢ A +_{ℎ} B = B +_{ℎ} A$
5	4	oveq1i	$⊢ (A +_{ℎ} B) +_{ℎ} C = (B +_{ℎ} A) +_{ℎ} C$
6	1 2 3	hvassi	$⊢ (A +_{ℎ} B) +_{ℎ} C = A +_{ℎ} (B +_{ℎ} C)$
7	2 1 3	hvassi	$⊢ (B +_{ℎ} A) +_{ℎ} C = B +_{ℎ} (A +_{ℎ} C)$
8	5 6 7	3eqtr3i	$⊢ A +_{ℎ} (B +_{ℎ} C) = B +_{ℎ} (A +_{ℎ} C)$