Metamath Proof Explorer

Theorem nvpncan2

Description: Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvpncan2.1 
|- X = ( BaseSet ` U )
nvpncan2.2 
|- G = ( +v ` U )
nvpncan2.3 
|- M = ( -v ` U )
Assertion nvpncan2 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M A ) = B )

Proof

Step Hyp Ref Expression
1 nvpncan2.1 
 |-  X = ( BaseSet ` U )
2 nvpncan2.2 
 |-  G = ( +v ` U )
3 nvpncan2.3 
 |-  M = ( -v ` U )
4 simp1 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> U e. NrmCVec )
5 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
6 simp2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> A e. X )
7 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
8 1 2 7 3 nvmval 
 |-  ( ( U e. NrmCVec /\ ( A G B ) e. X /\ A e. X ) -> ( ( A G B ) M A ) = ( ( A G B ) G ( -u 1 ( .sOLD ` U ) A ) ) )
9 4 5 6 8 syl3anc 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M A ) = ( ( A G B ) G ( -u 1 ( .sOLD ` U ) A ) ) )
10 simp3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> B e. X )
11 neg1cn 
 |-  -u 1 e. CC
12 1 7 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 ( .sOLD ` U ) A ) e. X )
13 11 12 mp3an2 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 ( .sOLD ` U ) A ) e. X )
14 13 3adant3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 ( .sOLD ` U ) A ) e. X )
15 1 2 nvadd32 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ ( -u 1 ( .sOLD ` U ) A ) e. X ) ) -> ( ( A G B ) G ( -u 1 ( .sOLD ` U ) A ) ) = ( ( A G ( -u 1 ( .sOLD ` U ) A ) ) G B ) )
16 4 6 10 14 15 syl13anc 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) G ( -u 1 ( .sOLD ` U ) A ) ) = ( ( A G ( -u 1 ( .sOLD ` U ) A ) ) G B ) )
17 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
18 1 2 7 17 nvrinv 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( -u 1 ( .sOLD ` U ) A ) ) = ( 0vec ` U ) )
19 18 3adant3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u 1 ( .sOLD ` U ) A ) ) = ( 0vec ` U ) )
20 19 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G ( -u 1 ( .sOLD ` U ) A ) ) G B ) = ( ( 0vec ` U ) G B ) )
21 1 2 17 nv0lid 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( ( 0vec ` U ) G B ) = B )
22 21 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( 0vec ` U ) G B ) = B )
23 20 22 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G ( -u 1 ( .sOLD ` U ) A ) ) G B ) = B )
24 16 23 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) G ( -u 1 ( .sOLD ` U ) A ) ) = B )
25 9 24 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M A ) = B )