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