Description: Subtractive distributive law for the scalar product of a subcomplex module. (Contributed by NM, 31-Jul-2007) (Revised by AV, 21-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clmpm1dir.v | |
|
clmpm1dir.s | |
||
clmpm1dir.a | |
||
clmpm1dir.k | |
||
Assertion | clmpm1dir | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clmpm1dir.v | |
|
2 | clmpm1dir.s | |
|
3 | clmpm1dir.a | |
|
4 | clmpm1dir.k | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | simpl | |
|
8 | simpr1 | |
|
9 | simpr2 | |
|
10 | simpr3 | |
|
11 | 1 2 5 4 6 7 8 9 10 | clmsubdir | |
12 | 1 5 2 4 | clmvscl | |
13 | 7 8 10 12 | syl3anc | |
14 | 1 5 2 4 | clmvscl | |
15 | 7 9 10 14 | syl3anc | |
16 | eqid | |
|
17 | 1 3 16 6 | grpsubval | |
18 | 13 15 17 | syl2anc | |
19 | 1 16 5 2 | clmvneg1 | |
20 | 19 | eqcomd | |
21 | 7 15 20 | syl2anc | |
22 | 21 | oveq2d | |
23 | 11 18 22 | 3eqtrd | |