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 ⊢W∈CMod∧A∈V∧B∈V∧C∈V∧D∈V→A+˙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 ⊢W∈CMod∧C∈V∧D∈V→W∈CMod
5 eqid ⊢Scalar⁡W=Scalar⁡W
6 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
7 5 6 clmneg1 ⊢W∈CMod→−1∈BaseScalar⁡W
8 7 adantr ⊢W∈CMod∧C∈V∧D∈V→−1∈BaseScalar⁡W
9 simpl ⊢C∈V∧D∈V→C∈V
10 9 adantl ⊢W∈CMod∧C∈V∧D∈V→C∈V
11 simpr ⊢C∈V∧D∈V→D∈V
12 11 adantl ⊢W∈CMod∧C∈V∧D∈V→D∈V
13 1 5 2 6 3 clmvsdi ⊢W∈CMod∧−1∈BaseScalar⁡W∧C∈V∧D∈V→-1·˙C+˙D=-1·˙C+˙-1·˙D
14 4 8 10 12 13 syl13anc ⊢W∈CMod∧C∈V∧D∈V→-1·˙C+˙D=-1·˙C+˙-1·˙D
15 14 3adant2 ⊢W∈CMod∧A∈V∧B∈V∧C∈V∧D∈V→-1·˙C+˙D=-1·˙C+˙-1·˙D
16 15 oveq2d ⊢W∈CMod∧A∈V∧B∈V∧C∈V∧D∈V→A+˙B+˙-1·˙C+˙D=A+˙B+˙-1·˙C+˙-1·˙D
17 clmabl ⊢W∈CMod→W∈Abel
18 ablcmn ⊢W∈Abel→W∈CMnd
19 17 18 syl ⊢W∈CMod→W∈CMnd
20 19 3ad2ant1 ⊢W∈CMod∧A∈V∧B∈V∧C∈V∧D∈V→W∈CMnd
21 simp2 ⊢W∈CMod∧A∈V∧B∈V∧C∈V∧D∈V→A∈V∧B∈V
22 simpl ⊢W∈CMod∧C∈V→W∈CMod
23 7 adantr ⊢W∈CMod∧C∈V→−1∈BaseScalar⁡W
24 simpr ⊢W∈CMod∧C∈V→C∈V
25 1 5 2 6 clmvscl ⊢W∈CMod∧−1∈BaseScalar⁡W∧C∈V→-1·˙C∈V
26 22 23 24 25 syl3anc ⊢W∈CMod∧C∈V→-1·˙C∈V
27 simpl ⊢W∈CMod∧D∈V→W∈CMod
28 7 adantr ⊢W∈CMod∧D∈V→−1∈BaseScalar⁡W
29 simpr ⊢W∈CMod∧D∈V→D∈V
30 1 5 2 6 clmvscl ⊢W∈CMod∧−1∈BaseScalar⁡W∧D∈V→-1·˙D∈V
31 27 28 29 30 syl3anc ⊢W∈CMod∧D∈V→-1·˙D∈V
32 26 31 anim12dan ⊢W∈CMod∧C∈V∧D∈V→-1·˙C∈V∧-1·˙D∈V
33 32 3adant2 ⊢W∈CMod∧A∈V∧B∈V∧C∈V∧D∈V→-1·˙C∈V∧-1·˙D∈V
34 1 3 cmn4 ⊢W∈CMnd∧A∈V∧B∈V∧-1·˙C∈V∧-1·˙D∈V→A+˙B+˙-1·˙C+˙-1·˙D=A+˙-1·˙C+˙B+˙-1·˙D
35 20 21 33 34 syl3anc ⊢W∈CMod∧A∈V∧B∈V∧C∈V∧D∈V→A+˙B+˙-1·˙C+˙-1·˙D=A+˙-1·˙C+˙B+˙-1·˙D
36 16 35 eqtrd ⊢W∈CMod∧A∈V∧B∈V∧C∈V∧D∈V→A+˙B+˙-1·˙C+˙D=A+˙-1·˙C+˙B+˙-1·˙D