Metamath Proof Explorer


Theorem nvaddsub4

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 X=BaseSetU
nvpncan2.2 G=+vU
nvpncan2.3 M=-vU
Assertion nvaddsub4 UNrmCVecAXBXCXDXAGBMCGD=AMCGBMD

Proof

Step Hyp Ref Expression
1 nvpncan2.1 X=BaseSetU
2 nvpncan2.2 G=+vU
3 nvpncan2.3 M=-vU
4 neg1cn 1
5 eqid 𝑠OLDU=𝑠OLDU
6 1 2 5 nvdi UNrmCVec1CXDX-1𝑠OLDUCGD=-1𝑠OLDUCG-1𝑠OLDUD
7 4 6 mp3anr1 UNrmCVecCXDX-1𝑠OLDUCGD=-1𝑠OLDUCG-1𝑠OLDUD
8 7 3adant2 UNrmCVecAXBXCXDX-1𝑠OLDUCGD=-1𝑠OLDUCG-1𝑠OLDUD
9 8 oveq2d UNrmCVecAXBXCXDXAGBG-1𝑠OLDUCGD=AGBG-1𝑠OLDUCG-1𝑠OLDUD
10 1 5 nvscl UNrmCVec1CX-1𝑠OLDUCX
11 4 10 mp3an2 UNrmCVecCX-1𝑠OLDUCX
12 1 5 nvscl UNrmCVec1DX-1𝑠OLDUDX
13 4 12 mp3an2 UNrmCVecDX-1𝑠OLDUDX
14 11 13 anim12dan UNrmCVecCXDX-1𝑠OLDUCX-1𝑠OLDUDX
15 14 3adant2 UNrmCVecAXBXCXDX-1𝑠OLDUCX-1𝑠OLDUDX
16 1 2 nvadd4 UNrmCVecAXBX-1𝑠OLDUCX-1𝑠OLDUDXAGBG-1𝑠OLDUCG-1𝑠OLDUD=AG-1𝑠OLDUCGBG-1𝑠OLDUD
17 15 16 syld3an3 UNrmCVecAXBXCXDXAGBG-1𝑠OLDUCG-1𝑠OLDUD=AG-1𝑠OLDUCGBG-1𝑠OLDUD
18 9 17 eqtrd UNrmCVecAXBXCXDXAGBG-1𝑠OLDUCGD=AG-1𝑠OLDUCGBG-1𝑠OLDUD
19 simp1 UNrmCVecAXBXCXDXUNrmCVec
20 1 2 nvgcl UNrmCVecAXBXAGBX
21 20 3expb UNrmCVecAXBXAGBX
22 21 3adant3 UNrmCVecAXBXCXDXAGBX
23 1 2 nvgcl UNrmCVecCXDXCGDX
24 23 3expb UNrmCVecCXDXCGDX
25 24 3adant2 UNrmCVecAXBXCXDXCGDX
26 1 2 5 3 nvmval UNrmCVecAGBXCGDXAGBMCGD=AGBG-1𝑠OLDUCGD
27 19 22 25 26 syl3anc UNrmCVecAXBXCXDXAGBMCGD=AGBG-1𝑠OLDUCGD
28 1 2 5 3 nvmval UNrmCVecAXCXAMC=AG-1𝑠OLDUC
29 28 3adant3r UNrmCVecAXCXDXAMC=AG-1𝑠OLDUC
30 29 3adant2r UNrmCVecAXBXCXDXAMC=AG-1𝑠OLDUC
31 1 2 5 3 nvmval UNrmCVecBXDXBMD=BG-1𝑠OLDUD
32 31 3adant3l UNrmCVecBXCXDXBMD=BG-1𝑠OLDUD
33 32 3adant2l UNrmCVecAXBXCXDXBMD=BG-1𝑠OLDUD
34 30 33 oveq12d UNrmCVecAXBXCXDXAMCGBMD=AG-1𝑠OLDUCGBG-1𝑠OLDUD
35 18 27 34 3eqtr4d UNrmCVecAXBXCXDXAGBMCGD=AMCGBMD