Metamath Proof Explorer


Theorem cphsubdir

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

Ref Expression
Hypotheses cphipcj.h ,˙=𝑖W
cphipcj.v V=BaseW
cphsubdir.m -˙=-W
Assertion cphsubdir WCPreHilAVBVCVA-˙B,˙C=A,˙CB,˙C

Proof

Step Hyp Ref Expression
1 cphipcj.h ,˙=𝑖W
2 cphipcj.v V=BaseW
3 cphsubdir.m -˙=-W
4 cphphl WCPreHilWPreHil
5 eqid ScalarW=ScalarW
6 eqid -ScalarW=-ScalarW
7 5 1 2 3 6 ipsubdir WPreHilAVBVCVA-˙B,˙C=A,˙C-ScalarWB,˙C
8 4 7 sylan WCPreHilAVBVCVA-˙B,˙C=A,˙C-ScalarWB,˙C
9 cphclm WCPreHilWCMod
10 9 adantr WCPreHilAVBVCVWCMod
11 4 adantr WCPreHilAVBVCVWPreHil
12 simpr1 WCPreHilAVBVCVAV
13 simpr3 WCPreHilAVBVCVCV
14 eqid BaseScalarW=BaseScalarW
15 5 1 2 14 ipcl WPreHilAVCVA,˙CBaseScalarW
16 11 12 13 15 syl3anc WCPreHilAVBVCVA,˙CBaseScalarW
17 simpr2 WCPreHilAVBVCVBV
18 5 1 2 14 ipcl WPreHilBVCVB,˙CBaseScalarW
19 11 17 13 18 syl3anc WCPreHilAVBVCVB,˙CBaseScalarW
20 5 14 clmsub WCModA,˙CBaseScalarWB,˙CBaseScalarWA,˙CB,˙C=A,˙C-ScalarWB,˙C
21 10 16 19 20 syl3anc WCPreHilAVBVCVA,˙CB,˙C=A,˙C-ScalarWB,˙C
22 8 21 eqtr4d WCPreHilAVBVCVA-˙B,˙C=A,˙CB,˙C