Description: Distributive law for inner product subtraction. Complex version of ipsubdir . (Contributed by Mario Carneiro, 16-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cphipcj.h | |
|
cphipcj.v | |
||
cphsubdir.m | |
||
Assertion | cphsubdir | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cphipcj.h | |
|
2 | cphipcj.v | |
|
3 | cphsubdir.m | |
|
4 | cphphl | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | 5 1 2 3 6 | ipsubdir | |
8 | 4 7 | sylan | |
9 | cphclm | |
|
10 | 9 | adantr | |
11 | 4 | adantr | |
12 | simpr1 | |
|
13 | simpr3 | |
|
14 | eqid | |
|
15 | 5 1 2 14 | ipcl | |
16 | 11 12 13 15 | syl3anc | |
17 | simpr2 | |
|
18 | 5 1 2 14 | ipcl | |
19 | 11 17 13 18 | syl3anc | |
20 | 5 14 | clmsub | |
21 | 10 16 19 20 | syl3anc | |
22 | 8 21 | eqtr4d | |