Metamath Proof Explorer


Theorem clmsub4

Description: Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 5-Aug-2007) (Revised by AV, 29-Sep-2021)

Ref Expression
Hypotheses clmpm1dir.v V=BaseW
clmpm1dir.s ·˙=W
clmpm1dir.a +˙=+W
Assertion clmsub4 WCModAVBVCVDVA+˙B+˙-1·˙C+˙D=A+˙-1·˙C+˙B+˙-1·˙D

Proof

Step Hyp Ref Expression
1 clmpm1dir.v V=BaseW
2 clmpm1dir.s ·˙=W
3 clmpm1dir.a +˙=+W
4 simpl WCModCVDVWCMod
5 eqid ScalarW=ScalarW
6 eqid BaseScalarW=BaseScalarW
7 5 6 clmneg1 WCMod1BaseScalarW
8 7 adantr WCModCVDV1BaseScalarW
9 simpl CVDVCV
10 9 adantl WCModCVDVCV
11 simpr CVDVDV
12 11 adantl WCModCVDVDV
13 1 5 2 6 3 clmvsdi WCMod1BaseScalarWCVDV-1·˙C+˙D=-1·˙C+˙-1·˙D
14 4 8 10 12 13 syl13anc WCModCVDV-1·˙C+˙D=-1·˙C+˙-1·˙D
15 14 3adant2 WCModAVBVCVDV-1·˙C+˙D=-1·˙C+˙-1·˙D
16 15 oveq2d WCModAVBVCVDVA+˙B+˙-1·˙C+˙D=A+˙B+˙-1·˙C+˙-1·˙D
17 clmabl WCModWAbel
18 ablcmn WAbelWCMnd
19 17 18 syl WCModWCMnd
20 19 3ad2ant1 WCModAVBVCVDVWCMnd
21 simp2 WCModAVBVCVDVAVBV
22 simpl WCModCVWCMod
23 7 adantr WCModCV1BaseScalarW
24 simpr WCModCVCV
25 1 5 2 6 clmvscl WCMod1BaseScalarWCV-1·˙CV
26 22 23 24 25 syl3anc WCModCV-1·˙CV
27 simpl WCModDVWCMod
28 7 adantr WCModDV1BaseScalarW
29 simpr WCModDVDV
30 1 5 2 6 clmvscl WCMod1BaseScalarWDV-1·˙DV
31 27 28 29 30 syl3anc WCModDV-1·˙DV
32 26 31 anim12dan WCModCVDV-1·˙CV-1·˙DV
33 32 3adant2 WCModAVBVCVDV-1·˙CV-1·˙DV
34 1 3 cmn4 WCMndAVBV-1·˙CV-1·˙DVA+˙B+˙-1·˙C+˙-1·˙D=A+˙-1·˙C+˙B+˙-1·˙D
35 20 21 33 34 syl3anc WCModAVBVCVDVA+˙B+˙-1·˙C+˙-1·˙D=A+˙-1·˙C+˙B+˙-1·˙D
36 16 35 eqtrd WCModAVBVCVDVA+˙B+˙-1·˙C+˙D=A+˙-1·˙C+˙B+˙-1·˙D