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

Metamath Proof Explorer

Theorem cphdir

Description: Distributive law for inner product (right-distributivity). Equation I3 of Ponnusamy p. 362. Complex version of ipdir . (Contributed by Mario Carneiro, 16-Oct-2015)

		Ref	Expression
	Hypotheses	cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
		cphipcj.v	$⊢ V = {Base}_{W}$
		cphdir.P	$⊢ \underset{˙}{+} = +_{W}$
	Assertion	cphdir	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{+} B) \underset{˙}{,} C = (A \underset{˙}{,} C) + (B \underset{˙}{,} C)$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
2		cphipcj.v	$⊢ V = {Base}_{W}$
3		cphdir.P	$⊢ \underset{˙}{+} = +_{W}$
4		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
5		eqid	$⊢ Scalar (W) = Scalar (W)$
6		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
7	5 1 2 3 6	ipdir	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{+} B) \underset{˙}{,} C = (A \underset{˙}{,} C) +_{Scalar (W)} (B \underset{˙}{,} C)$
8	4 7	sylan	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{+} B) \underset{˙}{,} C = (A \underset{˙}{,} C) +_{Scalar (W)} (B \underset{˙}{,} C)$
9		cphclm	$⊢ W \in CPreHil \to W \in CMod$
10	5	clmadd	$⊢ W \in CMod \to + = +_{Scalar (W)}$
11	9 10	syl	$⊢ W \in CPreHil \to + = +_{Scalar (W)}$
12	11	adantr	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to + = +_{Scalar (W)}$
13	12	oveqd	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{,} C) + (B \underset{˙}{,} C) = (A \underset{˙}{,} C) +_{Scalar (W)} (B \underset{˙}{,} C)$
14	8 13	eqtr4d	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{+} B) \underset{˙}{,} C = (A \underset{˙}{,} C) + (B \underset{˙}{,} C)$