Metamath Proof Explorer

Theorem hlmulass

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

	Ref	Expression
Hypotheses	hlmulf.1	$⊢ X = BaseSet (U)$
	hlmulf.4	$⊢ S = \cdot_{𝑠OLD} (U)$
Assertion	hlmulass	$⊢ (U \in {CHil}_{OLD} \land (A \in ℂ \land B \in ℂ \land C \in X)) \to A B S C = A S (B S C)$

Step	Hyp	Ref	Expression
1		hlmulf.1	$⊢ X = BaseSet (U)$
2		hlmulf.4	$⊢ S = \cdot_{𝑠OLD} (U)$
3		hlnv	$⊢ U \in {CHil}_{OLD} \to U \in NrmCVec$
4	1 2	nvsass	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in ℂ \land C \in X)) \to A B S C = A S (B S C)$
5	3 4	sylan	$⊢ (U \in {CHil}_{OLD} \land (A \in ℂ \land B \in ℂ \land C \in X)) \to A B S C = A S (B S C)$