Metamath Proof Explorer

Theorem hlass

Description: Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hladdf.1	$⊢ X = BaseSet (U)$
	hladdf.2	$⊢ G = +_{v} (U)$
Assertion	hlass	$⊢ (U \in {CHil}_{OLD} \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = A G (B G C)$

Step	Hyp	Ref	Expression
1		hladdf.1	$⊢ X = BaseSet (U)$
2		hladdf.2	$⊢ G = +_{v} (U)$
3		hlnv	$⊢ U \in {CHil}_{OLD} \to U \in NrmCVec$
4	1 2	nvass	$⊢ (U \in NrmCVec \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = A G (B G C)$
5	3 4	sylan	$⊢ (U \in {CHil}_{OLD} \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = A G (B G C)$