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	|- ., = ( .i ` W )
	cphipcj.v	|- V = ( Base ` W )
	cphdir.P	|- .+ = ( +g ` W )
Assertion	cphdir	|- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .+ B ) ., C ) = ( ( A ., C ) + ( B ., C ) ) )

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	|- ., = ( .i ` W )
2		cphipcj.v	|- V = ( Base ` W )
3		cphdir.P	|- .+ = ( +g ` W )
4		cphphl	|- ( W e. CPreHil -> W e. PreHil )
5		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
6		eqid	|- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
7	5 1 2 3 6	ipdir	|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .+ B ) ., C ) = ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) )
8	4 7	sylan	|- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .+ B ) ., C ) = ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) )
9		cphclm	|- ( W e. CPreHil -> W e. CMod )
10	5	clmadd	|- ( W e. CMod -> + = ( +g ` ( Scalar ` W ) ) )
11	9 10	syl	|- ( W e. CPreHil -> + = ( +g ` ( Scalar ` W ) ) )
12	11	adantr	|- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> + = ( +g ` ( Scalar ` W ) ) )
13	12	oveqd	|- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A ., C ) + ( B ., C ) ) = ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) )
14	8 13	eqtr4d	|- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .+ B ) ., C ) = ( ( A ., C ) + ( B ., C ) ) )