Metamath Proof Explorer

Theorem hlipdir

Description: Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		hlipdir.1	$⊢ X = BaseSet (U)$
2		hlipdir.2	$⊢ G = +_{v} (U)$
3		hlipdir.7	$⊢ P = \cdot_{𝑖OLD} (U)$
4		hlph	$⊢ U \in {CHil}_{OLD} \to U \in {CPreHil}_{OLD}$
5	1 2 3	dipdir	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in X \land C \in X)) \to (A G B) P C = (A P C) + (B P C)$
6	4 5	sylan	$⊢ (U \in {CHil}_{OLD} \land (A \in X \land B \in X \land C \in X)) \to (A G B) P C = (A P C) + (B P C)$