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 = ( BaseSet ` U )
nvpncan2.2 
|- G = ( +v ` U )
nvpncan2.3 
|- M = ( -v ` U )
Assertion nvaddsub4 
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) M ( C G D ) ) = ( ( A M C ) G ( B M D ) ) )

Proof

Step Hyp Ref Expression
1 nvpncan2.1 
 |-  X = ( BaseSet ` U )
2 nvpncan2.2 
 |-  G = ( +v ` U )
3 nvpncan2.3 
 |-  M = ( -v ` U )
4 neg1cn 
 |-  -u 1 e. CC
5 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
6 1 2 5 nvdi 
 |-  ( ( U e. NrmCVec /\ ( -u 1 e. CC /\ C e. X /\ D e. X ) ) -> ( -u 1 ( .sOLD ` U ) ( C G D ) ) = ( ( -u 1 ( .sOLD ` U ) C ) G ( -u 1 ( .sOLD ` U ) D ) ) )
7 4 6 mp3anr1 
 |-  ( ( U e. NrmCVec /\ ( C e. X /\ D e. X ) ) -> ( -u 1 ( .sOLD ` U ) ( C G D ) ) = ( ( -u 1 ( .sOLD ` U ) C ) G ( -u 1 ( .sOLD ` U ) D ) ) )
8 7 3adant2 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( -u 1 ( .sOLD ` U ) ( C G D ) ) = ( ( -u 1 ( .sOLD ` U ) C ) G ( -u 1 ( .sOLD ` U ) D ) ) )
9 8 oveq2d 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( -u 1 ( .sOLD ` U ) ( C G D ) ) ) = ( ( A G B ) G ( ( -u 1 ( .sOLD ` U ) C ) G ( -u 1 ( .sOLD ` U ) D ) ) ) )
10 1 5 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ C e. X ) -> ( -u 1 ( .sOLD ` U ) C ) e. X )
11 4 10 mp3an2 
 |-  ( ( U e. NrmCVec /\ C e. X ) -> ( -u 1 ( .sOLD ` U ) C ) e. X )
12 1 5 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ D e. X ) -> ( -u 1 ( .sOLD ` U ) D ) e. X )
13 4 12 mp3an2 
 |-  ( ( U e. NrmCVec /\ D e. X ) -> ( -u 1 ( .sOLD ` U ) D ) e. X )
14 11 13 anim12dan 
 |-  ( ( U e. NrmCVec /\ ( C e. X /\ D e. X ) ) -> ( ( -u 1 ( .sOLD ` U ) C ) e. X /\ ( -u 1 ( .sOLD ` U ) D ) e. X ) )
15 14 3adant2 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( -u 1 ( .sOLD ` U ) C ) e. X /\ ( -u 1 ( .sOLD ` U ) D ) e. X ) )
16 1 2 nvadd4 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( ( -u 1 ( .sOLD ` U ) C ) e. X /\ ( -u 1 ( .sOLD ` U ) D ) e. X ) ) -> ( ( A G B ) G ( ( -u 1 ( .sOLD ` U ) C ) G ( -u 1 ( .sOLD ` U ) D ) ) ) = ( ( A G ( -u 1 ( .sOLD ` U ) C ) ) G ( B G ( -u 1 ( .sOLD ` U ) D ) ) ) )
17 15 16 syld3an3 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( ( -u 1 ( .sOLD ` U ) C ) G ( -u 1 ( .sOLD ` U ) D ) ) ) = ( ( A G ( -u 1 ( .sOLD ` U ) C ) ) G ( B G ( -u 1 ( .sOLD ` U ) D ) ) ) )
18 9 17 eqtrd 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( -u 1 ( .sOLD ` U ) ( C G D ) ) ) = ( ( A G ( -u 1 ( .sOLD ` U ) C ) ) G ( B G ( -u 1 ( .sOLD ` U ) D ) ) ) )
19 simp1 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> U e. NrmCVec )
20 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
21 20 3expb 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( A G B ) e. X )
22 21 3adant3 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( A G B ) e. X )
23 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ C e. X /\ D e. X ) -> ( C G D ) e. X )
24 23 3expb 
 |-  ( ( U e. NrmCVec /\ ( C e. X /\ D e. X ) ) -> ( C G D ) e. X )
25 24 3adant2 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( C G D ) e. X )
26 1 2 5 3 nvmval 
 |-  ( ( U e. NrmCVec /\ ( A G B ) e. X /\ ( C G D ) e. X ) -> ( ( A G B ) M ( C G D ) ) = ( ( A G B ) G ( -u 1 ( .sOLD ` U ) ( C G D ) ) ) )
27 19 22 25 26 syl3anc 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) M ( C G D ) ) = ( ( A G B ) G ( -u 1 ( .sOLD ` U ) ( C G D ) ) ) )
28 1 2 5 3 nvmval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ C e. X ) -> ( A M C ) = ( A G ( -u 1 ( .sOLD ` U ) C ) ) )
29 28 3adant3r 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( C e. X /\ D e. X ) ) -> ( A M C ) = ( A G ( -u 1 ( .sOLD ` U ) C ) ) )
30 29 3adant2r 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( A M C ) = ( A G ( -u 1 ( .sOLD ` U ) C ) ) )
31 1 2 5 3 nvmval 
 |-  ( ( U e. NrmCVec /\ B e. X /\ D e. X ) -> ( B M D ) = ( B G ( -u 1 ( .sOLD ` U ) D ) ) )
32 31 3adant3l 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( C e. X /\ D e. X ) ) -> ( B M D ) = ( B G ( -u 1 ( .sOLD ` U ) D ) ) )
33 32 3adant2l 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( B M D ) = ( B G ( -u 1 ( .sOLD ` U ) D ) ) )
34 30 33 oveq12d 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A M C ) G ( B M D ) ) = ( ( A G ( -u 1 ( .sOLD ` U ) C ) ) G ( B G ( -u 1 ( .sOLD ` U ) D ) ) ) )
35 18 27 34 3eqtr4d 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) M ( C G D ) ) = ( ( A M C ) G ( B M D ) ) )