cph2subdi

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

	Ref	Expression
Hypotheses	cphipcj.h	\|- ., = ( .i ` W )
	cphipcj.v	\|- V = ( Base ` W )
	cphsubdir.m	\|- .- = ( -g ` W )
	cph2subdi.1	\|- ( ph -> W e. CPreHil )
	cph2subdi.2	\|- ( ph -> A e. V )
	cph2subdi.3	\|- ( ph -> B e. V )
	cph2subdi.4	\|- ( ph -> C e. V )
	cph2subdi.5	\|- ( ph -> D e. V )
Assertion	cph2subdi	\|- ( 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		cphsubdir.m	\|- .- = ( -g ` W )
4		cph2subdi.1	\|- ( ph -> W e. CPreHil )
5		cph2subdi.2	\|- ( ph -> A e. V )
6		cph2subdi.3	\|- ( ph -> B e. V )
7		cph2subdi.4	\|- ( ph -> C e. V )
8		cph2subdi.5	\|- ( ph -> D e. V )
9		cphclm	\|- ( W e. CPreHil -> W e. CMod )
10	4 9	syl	\|- ( ph -> W e. CMod )
11		eqid	\|- ( Scalar ` W ) = ( Scalar ` W )
12	11	clmadd	\|- ( W e. CMod -> + = ( +g ` ( Scalar ` W ) ) )
13	10 12	syl	\|- ( ph -> + = ( +g ` ( Scalar ` W ) ) )
14	13	oveqd	\|- ( ph -> ( ( A ., C ) + ( B ., D ) ) = ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) )
15	13	oveqd	\|- ( ph -> ( ( A ., D ) + ( B ., C ) ) = ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) )
16	14 15	oveq12d	\|- ( ph -> ( ( ( A ., C ) + ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) + ( B ., C ) ) ) = ( ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) )
17		cphphl	\|- ( W e. CPreHil -> W e. PreHil )
18	4 17	syl	\|- ( ph -> W e. PreHil )
19		eqid	\|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
20	11 1 2 19	ipcl	\|- ( ( W e. PreHil /\ A e. V /\ C e. V ) -> ( A ., C ) e. ( Base ` ( Scalar ` W ) ) )
21	18 5 7 20	syl3anc	\|- ( ph -> ( A ., C ) e. ( Base ` ( Scalar ` W ) ) )
22	11 1 2 19	ipcl	\|- ( ( W e. PreHil /\ B e. V /\ D e. V ) -> ( B ., D ) e. ( Base ` ( Scalar ` W ) ) )
23	18 6 8 22	syl3anc	\|- ( ph -> ( B ., D ) e. ( Base ` ( Scalar ` W ) ) )
24	11 19	clmacl	\|- ( ( W e. CMod /\ ( A ., C ) e. ( Base ` ( Scalar ` W ) ) /\ ( B ., D ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( A ., C ) + ( B ., D ) ) e. ( Base ` ( Scalar ` W ) ) )
25	10 21 23 24	syl3anc	\|- ( ph -> ( ( A ., C ) + ( B ., D ) ) e. ( Base ` ( Scalar ` W ) ) )
26	11 1 2 19	ipcl	\|- ( ( W e. PreHil /\ A e. V /\ D e. V ) -> ( A ., D ) e. ( Base ` ( Scalar ` W ) ) )
27	18 5 8 26	syl3anc	\|- ( ph -> ( A ., D ) e. ( Base ` ( Scalar ` W ) ) )
28	11 1 2 19	ipcl	\|- ( ( W e. PreHil /\ B e. V /\ C e. V ) -> ( B ., C ) e. ( Base ` ( Scalar ` W ) ) )
29	18 6 7 28	syl3anc	\|- ( ph -> ( B ., C ) e. ( Base ` ( Scalar ` W ) ) )
30	11 19	clmacl	\|- ( ( W e. CMod /\ ( A ., D ) e. ( Base ` ( Scalar ` W ) ) /\ ( B ., C ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( A ., D ) + ( B ., C ) ) e. ( Base ` ( Scalar ` W ) ) )
31	10 27 29 30	syl3anc	\|- ( ph -> ( ( A ., D ) + ( B ., C ) ) e. ( Base ` ( Scalar ` W ) ) )
32	11 19	clmsub	\|- ( ( W e. CMod /\ ( ( A ., C ) + ( B ., D ) ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( A ., D ) + ( B ., C ) ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) = ( ( ( A ., C ) + ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) + ( B ., C ) ) ) )
33	10 25 31 32	syl3anc	\|- ( ph -> ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) = ( ( ( A ., C ) + ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) + ( B ., C ) ) ) )
34		eqid	\|- ( -g ` ( Scalar ` W ) ) = ( -g ` ( Scalar ` W ) )
35		eqid	\|- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
36	11 1 2 3 34 35 18 5 6 7 8	ip2subdi	\|- ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) )
37	16 33 36	3eqtr4rd	\|- ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) )

Metamath Proof Explorer

Theorem cph2subdi

Proof