Metamath Proof Explorer


Theorem cphsubdi

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

Ref Expression
Hypotheses cphipcj.h , ˙ = 𝑖 W
cphipcj.v V = Base W
cphsubdir.m - ˙ = - W
Assertion cphsubdi W CPreHil A V B V C V A , ˙ B - ˙ C = A , ˙ B A , ˙ C

Proof

Step Hyp Ref Expression
1 cphipcj.h , ˙ = 𝑖 W
2 cphipcj.v V = Base W
3 cphsubdir.m - ˙ = - W
4 cphphl W CPreHil W PreHil
5 eqid Scalar W = Scalar W
6 eqid - Scalar W = - Scalar W
7 5 1 2 3 6 ipsubdi W PreHil A V B V C V A , ˙ B - ˙ C = A , ˙ B - Scalar W A , ˙ C
8 4 7 sylan W CPreHil A V B V C V A , ˙ B - ˙ C = A , ˙ B - Scalar W A , ˙ C
9 cphclm W CPreHil W CMod
10 9 adantr W CPreHil A V B V C V W CMod
11 4 adantr W CPreHil A V B V C V W PreHil
12 simpr1 W CPreHil A V B V C V A V
13 simpr2 W CPreHil A V B V C V B V
14 eqid Base Scalar W = Base Scalar W
15 5 1 2 14 ipcl W PreHil A V B V A , ˙ B Base Scalar W
16 11 12 13 15 syl3anc W CPreHil A V B V C V A , ˙ B Base Scalar W
17 simpr3 W CPreHil A V B V C V C V
18 5 1 2 14 ipcl W PreHil A V C V A , ˙ C Base Scalar W
19 11 12 17 18 syl3anc W CPreHil A V B V C V A , ˙ C Base Scalar W
20 5 14 clmsub W CMod A , ˙ B Base Scalar W A , ˙ C Base Scalar W A , ˙ B A , ˙ C = A , ˙ B - Scalar W A , ˙ C
21 10 16 19 20 syl3anc W CPreHil A V B V C V A , ˙ B A , ˙ C = A , ˙ B - Scalar W A , ˙ C
22 8 21 eqtr4d W CPreHil A V B V C V A , ˙ B - ˙ C = A , ˙ B A , ˙ C