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 | |
|
clmpm1dir.s | |
||
clmpm1dir.a | |
||
Assertion | clmsub4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clmpm1dir.v | |
|
2 | clmpm1dir.s | |
|
3 | clmpm1dir.a | |
|
4 | simpl | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | 5 6 | clmneg1 | |
8 | 7 | adantr | |
9 | simpl | |
|
10 | 9 | adantl | |
11 | simpr | |
|
12 | 11 | adantl | |
13 | 1 5 2 6 3 | clmvsdi | |
14 | 4 8 10 12 13 | syl13anc | |
15 | 14 | 3adant2 | |
16 | 15 | oveq2d | |
17 | clmabl | |
|
18 | ablcmn | |
|
19 | 17 18 | syl | |
20 | 19 | 3ad2ant1 | |
21 | simp2 | |
|
22 | simpl | |
|
23 | 7 | adantr | |
24 | simpr | |
|
25 | 1 5 2 6 | clmvscl | |
26 | 22 23 24 25 | syl3anc | |
27 | simpl | |
|
28 | 7 | adantr | |
29 | simpr | |
|
30 | 1 5 2 6 | clmvscl | |
31 | 27 28 29 30 | syl3anc | |
32 | 26 31 | anim12dan | |
33 | 32 | 3adant2 | |
34 | 1 3 | cmn4 | |
35 | 20 21 33 34 | syl3anc | |
36 | 16 35 | eqtrd | |