Metamath Proof Explorer

Theorem hldi

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

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

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