Metamath Proof Explorer

Theorem dipsubdir

Description: Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipsubdir.1 
|- X = ( BaseSet ` U )
ipsubdir.3 
|- M = ( -v ` U )
ipsubdir.7 
|- P = ( .iOLD ` U )
Assertion dipsubdir 
|- ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) P C ) = ( ( A P C ) - ( B P C ) ) )

Proof

Step Hyp Ref Expression
1 ipsubdir.1 
 |-  X = ( BaseSet ` U )
2 ipsubdir.3 
 |-  M = ( -v ` U )
3 ipsubdir.7 
 |-  P = ( .iOLD ` U )
4 idd 
 |-  ( U e. CPreHilOLD -> ( A e. X -> A e. X ) )
5 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
6 neg1cn 
 |-  -u 1 e. CC
7 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
8 1 7 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 ( .sOLD ` U ) B ) e. X )
9 6 8 mp3an2 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 ( .sOLD ` U ) B ) e. X )
10 5 9 sylan 
 |-  ( ( U e. CPreHilOLD /\ B e. X ) -> ( -u 1 ( .sOLD ` U ) B ) e. X )
11 10 ex 
 |-  ( U e. CPreHilOLD -> ( B e. X -> ( -u 1 ( .sOLD ` U ) B ) e. X ) )
12 idd 
 |-  ( U e. CPreHilOLD -> ( C e. X -> C e. X ) )
13 4 11 12 3anim123d 
 |-  ( U e. CPreHilOLD -> ( ( A e. X /\ B e. X /\ C e. X ) -> ( A e. X /\ ( -u 1 ( .sOLD ` U ) B ) e. X /\ C e. X ) ) )
14 13 imp 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A e. X /\ ( -u 1 ( .sOLD ` U ) B ) e. X /\ C e. X ) )
15 eqid 
 |-  ( +v ` U ) = ( +v ` U )
16 1 15 3 dipdir 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ ( -u 1 ( .sOLD ` U ) B ) e. X /\ C e. X ) ) -> ( ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) P C ) = ( ( A P C ) + ( ( -u 1 ( .sOLD ` U ) B ) P C ) ) )
17 14 16 syldan 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) P C ) = ( ( A P C ) + ( ( -u 1 ( .sOLD ` U ) B ) P C ) ) )
18 1 15 7 2 nvmval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
19 5 18 syl3an1 
 |-  ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> ( A M B ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
20 19 3adant3r3 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A M B ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
21 20 oveq1d 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) P C ) = ( ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) P C ) )
22 1 7 3 dipass 
 |-  ( ( U e. CPreHilOLD /\ ( -u 1 e. CC /\ B e. X /\ C e. X ) ) -> ( ( -u 1 ( .sOLD ` U ) B ) P C ) = ( -u 1 x. ( B P C ) ) )
23 6 22 mp3anr1 
 |-  ( ( U e. CPreHilOLD /\ ( B e. X /\ C e. X ) ) -> ( ( -u 1 ( .sOLD ` U ) B ) P C ) = ( -u 1 x. ( B P C ) ) )
24 1 3 dipcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ C e. X ) -> ( B P C ) e. CC )
25 24 3expb 
 |-  ( ( U e. NrmCVec /\ ( B e. X /\ C e. X ) ) -> ( B P C ) e. CC )
26 5 25 sylan 
 |-  ( ( U e. CPreHilOLD /\ ( B e. X /\ C e. X ) ) -> ( B P C ) e. CC )
27 26 mulm1d 
 |-  ( ( U e. CPreHilOLD /\ ( B e. X /\ C e. X ) ) -> ( -u 1 x. ( B P C ) ) = -u ( B P C ) )
28 23 27 eqtrd 
 |-  ( ( U e. CPreHilOLD /\ ( B e. X /\ C e. X ) ) -> ( ( -u 1 ( .sOLD ` U ) B ) P C ) = -u ( B P C ) )
29 28 3adantr1 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( -u 1 ( .sOLD ` U ) B ) P C ) = -u ( B P C ) )
30 29 oveq2d 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A P C ) + ( ( -u 1 ( .sOLD ` U ) B ) P C ) ) = ( ( A P C ) + -u ( B P C ) ) )
31 1 3 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ C e. X ) -> ( A P C ) e. CC )
32 31 3adant3r2 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A P C ) e. CC )
33 24 3adant3r1 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B P C ) e. CC )
34 32 33 negsubd 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A P C ) + -u ( B P C ) ) = ( ( A P C ) - ( B P C ) ) )
35 5 34 sylan 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A P C ) + -u ( B P C ) ) = ( ( A P C ) - ( B P C ) ) )
36 30 35 eqtr2d 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A P C ) - ( B P C ) ) = ( ( A P C ) + ( ( -u 1 ( .sOLD ` U ) B ) P C ) ) )
37 17 21 36 3eqtr4d 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) P C ) = ( ( A P C ) - ( B P C ) ) )