Description: Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 8-Feb-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nvpncan2.1 | |
|
nvpncan2.2 | |
||
nvpncan2.3 | |
||
Assertion | nvaddsub4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvpncan2.1 | |
|
2 | nvpncan2.2 | |
|
3 | nvpncan2.3 | |
|
4 | neg1cn | |
|
5 | eqid | |
|
6 | 1 2 5 | nvdi | |
7 | 4 6 | mp3anr1 | |
8 | 7 | 3adant2 | |
9 | 8 | oveq2d | |
10 | 1 5 | nvscl | |
11 | 4 10 | mp3an2 | |
12 | 1 5 | nvscl | |
13 | 4 12 | mp3an2 | |
14 | 11 13 | anim12dan | |
15 | 14 | 3adant2 | |
16 | 1 2 | nvadd4 | |
17 | 15 16 | syld3an3 | |
18 | 9 17 | eqtrd | |
19 | simp1 | |
|
20 | 1 2 | nvgcl | |
21 | 20 | 3expb | |
22 | 21 | 3adant3 | |
23 | 1 2 | nvgcl | |
24 | 23 | 3expb | |
25 | 24 | 3adant2 | |
26 | 1 2 5 3 | nvmval | |
27 | 19 22 25 26 | syl3anc | |
28 | 1 2 5 3 | nvmval | |
29 | 28 | 3adant3r | |
30 | 29 | 3adant2r | |
31 | 1 2 5 3 | nvmval | |
32 | 31 | 3adant3l | |
33 | 32 | 3adant2l | |
34 | 30 33 | oveq12d | |
35 | 18 27 34 | 3eqtr4d | |