Metamath Proof Explorer


Theorem clmpm1dir

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 V=BaseW
clmpm1dir.s ·˙=W
clmpm1dir.a +˙=+W
clmpm1dir.k K=BaseScalarW
Assertion clmpm1dir WCModAKBKCVAB·˙C=A·˙C+˙-1·˙B·˙C

Proof

Step Hyp Ref Expression
1 clmpm1dir.v V=BaseW
2 clmpm1dir.s ·˙=W
3 clmpm1dir.a +˙=+W
4 clmpm1dir.k K=BaseScalarW
5 eqid ScalarW=ScalarW
6 eqid -W=-W
7 simpl WCModAKBKCVWCMod
8 simpr1 WCModAKBKCVAK
9 simpr2 WCModAKBKCVBK
10 simpr3 WCModAKBKCVCV
11 1 2 5 4 6 7 8 9 10 clmsubdir WCModAKBKCVAB·˙C=A·˙C-WB·˙C
12 1 5 2 4 clmvscl WCModAKCVA·˙CV
13 7 8 10 12 syl3anc WCModAKBKCVA·˙CV
14 1 5 2 4 clmvscl WCModBKCVB·˙CV
15 7 9 10 14 syl3anc WCModAKBKCVB·˙CV
16 eqid invgW=invgW
17 1 3 16 6 grpsubval A·˙CVB·˙CVA·˙C-WB·˙C=A·˙C+˙invgWB·˙C
18 13 15 17 syl2anc WCModAKBKCVA·˙C-WB·˙C=A·˙C+˙invgWB·˙C
19 1 16 5 2 clmvneg1 WCModB·˙CV-1·˙B·˙C=invgWB·˙C
20 19 eqcomd WCModB·˙CVinvgWB·˙C=-1·˙B·˙C
21 7 15 20 syl2anc WCModAKBKCVinvgWB·˙C=-1·˙B·˙C
22 21 oveq2d WCModAKBKCVA·˙C+˙invgWB·˙C=A·˙C+˙-1·˙B·˙C
23 11 18 22 3eqtrd WCModAKBKCVAB·˙C=A·˙C+˙-1·˙B·˙C