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 ) ) )