Metamath Proof Explorer

Theorem nvmdi

Description: Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvmdi.1 
|- X = ( BaseSet ` U )
nvmdi.3 
|- M = ( -v ` U )
nvmdi.4 
|- S = ( .sOLD ` U )
Assertion nvmdi 
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B M C ) ) = ( ( A S B ) M ( A S C ) ) )

Proof

Step Hyp Ref Expression
1 nvmdi.1 
 |-  X = ( BaseSet ` U )
2 nvmdi.3 
 |-  M = ( -v ` U )
3 nvmdi.4 
 |-  S = ( .sOLD ` U )
4 simpr1 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> A e. CC )
5 simpr2 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> B e. X )
6 neg1cn 
 |-  -u 1 e. CC
7 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ C e. X ) -> ( -u 1 S C ) e. X )
8 6 7 mp3an2 
 |-  ( ( U e. NrmCVec /\ C e. X ) -> ( -u 1 S C ) e. X )
9 8 3ad2antr3 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( -u 1 S C ) e. X )
10 4 5 9 3jca 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A e. CC /\ B e. X /\ ( -u 1 S C ) e. X ) )
11 eqid 
 |-  ( +v ` U ) = ( +v ` U )
12 1 11 3 nvdi 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ ( -u 1 S C ) e. X ) ) -> ( A S ( B ( +v ` U ) ( -u 1 S C ) ) ) = ( ( A S B ) ( +v ` U ) ( A S ( -u 1 S C ) ) ) )
13 10 12 syldan 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B ( +v ` U ) ( -u 1 S C ) ) ) = ( ( A S B ) ( +v ` U ) ( A S ( -u 1 S C ) ) ) )
14 1 3 nvscom 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ -u 1 e. CC /\ C e. X ) ) -> ( A S ( -u 1 S C ) ) = ( -u 1 S ( A S C ) ) )
15 6 14 mp3anr2 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ C e. X ) ) -> ( A S ( -u 1 S C ) ) = ( -u 1 S ( A S C ) ) )
16 15 3adantr2 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( -u 1 S C ) ) = ( -u 1 S ( A S C ) ) )
17 16 oveq2d 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( ( A S B ) ( +v ` U ) ( A S ( -u 1 S C ) ) ) = ( ( A S B ) ( +v ` U ) ( -u 1 S ( A S C ) ) ) )
18 13 17 eqtrd 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B ( +v ` U ) ( -u 1 S C ) ) ) = ( ( A S B ) ( +v ` U ) ( -u 1 S ( A S C ) ) ) )
19 1 11 3 2 nvmval 
 |-  ( ( U e. NrmCVec /\ B e. X /\ C e. X ) -> ( B M C ) = ( B ( +v ` U ) ( -u 1 S C ) ) )
20 19 3adant3r1 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( B M C ) = ( B ( +v ` U ) ( -u 1 S C ) ) )
21 20 oveq2d 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B M C ) ) = ( A S ( B ( +v ` U ) ( -u 1 S C ) ) ) )
22 simpl 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> U e. NrmCVec )
23 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( A S B ) e. X )
24 23 3adant3r3 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S B ) e. X )
25 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ C e. X ) -> ( A S C ) e. X )
26 25 3adant3r2 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S C ) e. X )
27 1 11 3 2 nvmval 
 |-  ( ( U e. NrmCVec /\ ( A S B ) e. X /\ ( A S C ) e. X ) -> ( ( A S B ) M ( A S C ) ) = ( ( A S B ) ( +v ` U ) ( -u 1 S ( A S C ) ) ) )
28 22 24 26 27 syl3anc 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( ( A S B ) M ( A S C ) ) = ( ( A S B ) ( +v ` U ) ( -u 1 S ( A S C ) ) ) )
29 18 21 28 3eqtr4d 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B M C ) ) = ( ( A S B ) M ( A S C ) ) )