Theorem cph2di

Description: Distributive law for inner product. Complex version of ip2di . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	|- ., = ( .i ` W )
	cphipcj.v	|- V = ( Base ` W )
	cphdir.P	|- .+ = ( +g ` W )
	cph2di.1	|- ( ph -> W e. CPreHil )
	cph2di.2	|- ( ph -> A e. V )
	cph2di.3	|- ( ph -> B e. V )
	cph2di.4	|- ( ph -> C e. V )
	cph2di.5	|- ( ph -> D e. V )
Assertion	cph2di	|- ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) + ( B ., D ) ) + ( ( A ., D ) + ( B ., C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	|- ., = ( .i ` W )
2		cphipcj.v	|- V = ( Base ` W )
3		cphdir.P	|- .+ = ( +g ` W )
4		cph2di.1	|- ( ph -> W e. CPreHil )
5		cph2di.2	|- ( ph -> A e. V )
6		cph2di.3	|- ( ph -> B e. V )
7		cph2di.4	|- ( ph -> C e. V )
8		cph2di.5	|- ( ph -> D e. V )
9		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
10		eqid	|- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
11		cphphl	|- ( W e. CPreHil -> W e. PreHil )
12	4 11	syl	|- ( ph -> W e. PreHil )
13	9 1 2 3 10 12 5 6 7 8	ip2di	|- ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ( +g ` ( Scalar ` W ) ) ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) )
14		cphclm	|- ( W e. CPreHil -> W e. CMod )
15	9	clmadd	|- ( W e. CMod -> + = ( +g ` ( Scalar ` W ) ) )
16	4 14 15	3syl	|- ( ph -> + = ( +g ` ( Scalar ` W ) ) )
17	16	oveqd	|- ( ph -> ( ( A ., C ) + ( B ., D ) ) = ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) )
18	16	oveqd	|- ( ph -> ( ( A ., D ) + ( B ., C ) ) = ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) )
19	16 17 18	oveq123d	|- ( ph -> ( ( ( A ., C ) + ( B ., D ) ) + ( ( A ., D ) + ( B ., C ) ) ) = ( ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ( +g ` ( Scalar ` W ) ) ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) )
20	13 19	eqtr4d	|- ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) + ( B ., D ) ) + ( ( A ., D ) + ( B ., C ) ) ) )