# Metamath Proof Explorer

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 )`
`|- ( ( 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 ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( U e. NrmCVec /\ A e. X /\ ( C e. X /\ D e. X ) ) -> ( A M C ) = ( A G ( -u 1 ( .sOLD ` U ) C ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( U e. NrmCVec /\ B e. X /\ D e. X ) -> ( B M D ) = ( B G ( -u 1 ( .sOLD ` U ) D ) ) )`
` |-  ( ( U e. NrmCVec /\ B e. X /\ ( C e. X /\ D e. X ) ) -> ( B M D ) = ( B G ( -u 1 ( .sOLD ` U ) D ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) )`