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 = Base W
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 = Base W
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 ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
7 5 6 clmneg1 ⊢ W ∈ CMod → − 1 ∈ Base Scalar ⁡ W
8 7 adantr ⊢ W ∈ CMod ∧ C ∈ V ∧ D ∈ V → − 1 ∈ Base Scalar ⁡ 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 ∈ Base Scalar ⁡ 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 ∈ Base Scalar ⁡ W
24 simpr ⊢ W ∈ CMod ∧ C ∈ V → C ∈ V
25 1 5 2 6 clmvscl ⊢ W ∈ CMod ∧ − 1 ∈ Base Scalar ⁡ 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 ∈ Base Scalar ⁡ W
29 simpr ⊢ W ∈ CMod ∧ D ∈ V → D ∈ V
30 1 5 2 6 clmvscl ⊢ W ∈ CMod ∧ − 1 ∈ Base Scalar ⁡ 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