Metamath Proof Explorer

Theorem ipasslem2

Description: Lemma for ipassi . Show the inner product associative law for nonpositive integers. (Contributed by NM, 27-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 
|- X = ( BaseSet ` U )
ip1i.2 
|- G = ( +v ` U )
ip1i.4 
|- S = ( .sOLD ` U )
ip1i.7 
|- P = ( .iOLD ` U )
ip1i.9 
|- U e. CPreHilOLD
ipasslem1.b 
|- B e. X
Assertion ipasslem2 
|- ( ( N e. NN0 /\ A e. X ) -> ( ( -u N S A ) P B ) = ( -u N x. ( A P B ) ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 
 |-  X = ( BaseSet ` U )
2 ip1i.2 
 |-  G = ( +v ` U )
3 ip1i.4 
 |-  S = ( .sOLD ` U )
4 ip1i.7 
 |-  P = ( .iOLD ` U )
5 ip1i.9 
 |-  U e. CPreHilOLD
6 ipasslem1.b 
 |-  B e. X
7 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
8 7 negcld 
 |-  ( N e. NN0 -> -u N e. CC )
9 5 phnvi 
 |-  U e. NrmCVec
10 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
11 9 6 10 mp3an13 
 |-  ( A e. X -> ( A P B ) e. CC )
12 mulcl 
 |-  ( ( -u N e. CC /\ ( A P B ) e. CC ) -> ( -u N x. ( A P B ) ) e. CC )
13 8 11 12 syl2an 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( -u N x. ( A P B ) ) e. CC )
14 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u N e. CC /\ A e. X ) -> ( -u N S A ) e. X )
15 9 14 mp3an1 
 |-  ( ( -u N e. CC /\ A e. X ) -> ( -u N S A ) e. X )
16 8 15 sylan 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( -u N S A ) e. X )
17 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ ( -u N S A ) e. X /\ B e. X ) -> ( ( -u N S A ) P B ) e. CC )
18 9 6 17 mp3an13 
 |-  ( ( -u N S A ) e. X -> ( ( -u N S A ) P B ) e. CC )
19 16 18 syl 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N S A ) P B ) e. CC )
20 ax-1cn 
 |-  1 e. CC
21 mulneg2 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N x. -u 1 ) = -u ( N x. 1 ) )
22 20 21 mpan2 
 |-  ( N e. CC -> ( N x. -u 1 ) = -u ( N x. 1 ) )
23 mulid1 
 |-  ( N e. CC -> ( N x. 1 ) = N )
24 23 negeqd 
 |-  ( N e. CC -> -u ( N x. 1 ) = -u N )
25 22 24 eqtr2d 
 |-  ( N e. CC -> -u N = ( N x. -u 1 ) )
26 25 adantr 
 |-  ( ( N e. CC /\ A e. X ) -> -u N = ( N x. -u 1 ) )
27 26 oveq1d 
 |-  ( ( N e. CC /\ A e. X ) -> ( -u N S A ) = ( ( N x. -u 1 ) S A ) )
28 neg1cn 
 |-  -u 1 e. CC
29 1 3 nvsass 
 |-  ( ( U e. NrmCVec /\ ( N e. CC /\ -u 1 e. CC /\ A e. X ) ) -> ( ( N x. -u 1 ) S A ) = ( N S ( -u 1 S A ) ) )
30 9 29 mpan 
 |-  ( ( N e. CC /\ -u 1 e. CC /\ A e. X ) -> ( ( N x. -u 1 ) S A ) = ( N S ( -u 1 S A ) ) )
31 28 30 mp3an2 
 |-  ( ( N e. CC /\ A e. X ) -> ( ( N x. -u 1 ) S A ) = ( N S ( -u 1 S A ) ) )
32 27 31 eqtrd 
 |-  ( ( N e. CC /\ A e. X ) -> ( -u N S A ) = ( N S ( -u 1 S A ) ) )
33 7 32 sylan 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( -u N S A ) = ( N S ( -u 1 S A ) ) )
34 33 oveq1d 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N S A ) P B ) = ( ( N S ( -u 1 S A ) ) P B ) )
35 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 S A ) e. X )
36 9 28 35 mp3an12 
 |-  ( A e. X -> ( -u 1 S A ) e. X )
37 1 2 3 4 5 6 ipasslem1 
 |-  ( ( N e. NN0 /\ ( -u 1 S A ) e. X ) -> ( ( N S ( -u 1 S A ) ) P B ) = ( N x. ( ( -u 1 S A ) P B ) ) )
38 36 37 sylan2 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( N S ( -u 1 S A ) ) P B ) = ( N x. ( ( -u 1 S A ) P B ) ) )
39 34 38 eqtrd 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N S A ) P B ) = ( N x. ( ( -u 1 S A ) P B ) ) )
40 39 oveq2d 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N x. ( A P B ) ) - ( ( -u N S A ) P B ) ) = ( ( -u N x. ( A P B ) ) - ( N x. ( ( -u 1 S A ) P B ) ) ) )
41 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ ( -u 1 S A ) e. X /\ B e. X ) -> ( ( -u 1 S A ) P B ) e. CC )
42 9 6 41 mp3an13 
 |-  ( ( -u 1 S A ) e. X -> ( ( -u 1 S A ) P B ) e. CC )
43 36 42 syl 
 |-  ( A e. X -> ( ( -u 1 S A ) P B ) e. CC )
44 mulcl 
 |-  ( ( N e. CC /\ ( ( -u 1 S A ) P B ) e. CC ) -> ( N x. ( ( -u 1 S A ) P B ) ) e. CC )
45 7 43 44 syl2an 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( N x. ( ( -u 1 S A ) P B ) ) e. CC )
46 13 45 negsubd 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N x. ( A P B ) ) + -u ( N x. ( ( -u 1 S A ) P B ) ) ) = ( ( -u N x. ( A P B ) ) - ( N x. ( ( -u 1 S A ) P B ) ) ) )
47 mulneg1 
 |-  ( ( N e. CC /\ ( ( -u 1 S A ) P B ) e. CC ) -> ( -u N x. ( ( -u 1 S A ) P B ) ) = -u ( N x. ( ( -u 1 S A ) P B ) ) )
48 7 43 47 syl2an 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( -u N x. ( ( -u 1 S A ) P B ) ) = -u ( N x. ( ( -u 1 S A ) P B ) ) )
49 48 oveq2d 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N x. ( A P B ) ) + ( -u N x. ( ( -u 1 S A ) P B ) ) ) = ( ( -u N x. ( A P B ) ) + -u ( N x. ( ( -u 1 S A ) P B ) ) ) )
50 8 adantr 
 |-  ( ( N e. NN0 /\ A e. X ) -> -u N e. CC )
51 11 adantl 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( A P B ) e. CC )
52 43 adantl 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u 1 S A ) P B ) e. CC )
53 50 51 52 adddid 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( -u N x. ( ( A P B ) + ( ( -u 1 S A ) P B ) ) ) = ( ( -u N x. ( A P B ) ) + ( -u N x. ( ( -u 1 S A ) P B ) ) ) )
54 1 2 3 4 5 ipdiri 
 |-  ( ( A e. X /\ ( -u 1 S A ) e. X /\ B e. X ) -> ( ( A G ( -u 1 S A ) ) P B ) = ( ( A P B ) + ( ( -u 1 S A ) P B ) ) )
55 6 54 mp3an3 
 |-  ( ( A e. X /\ ( -u 1 S A ) e. X ) -> ( ( A G ( -u 1 S A ) ) P B ) = ( ( A P B ) + ( ( -u 1 S A ) P B ) ) )
56 36 55 mpdan 
 |-  ( A e. X -> ( ( A G ( -u 1 S A ) ) P B ) = ( ( A P B ) + ( ( -u 1 S A ) P B ) ) )
57 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
58 1 2 3 57 nvrinv 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( -u 1 S A ) ) = ( 0vec ` U ) )
59 9 58 mpan 
 |-  ( A e. X -> ( A G ( -u 1 S A ) ) = ( 0vec ` U ) )
60 59 oveq1d 
 |-  ( A e. X -> ( ( A G ( -u 1 S A ) ) P B ) = ( ( 0vec ` U ) P B ) )
61 1 57 4 dip0l 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( ( 0vec ` U ) P B ) = 0 )
62 9 6 61 mp2an 
 |-  ( ( 0vec ` U ) P B ) = 0
63 60 62 eqtrdi 
 |-  ( A e. X -> ( ( A G ( -u 1 S A ) ) P B ) = 0 )
64 56 63 eqtr3d 
 |-  ( A e. X -> ( ( A P B ) + ( ( -u 1 S A ) P B ) ) = 0 )
65 64 oveq2d 
 |-  ( A e. X -> ( -u N x. ( ( A P B ) + ( ( -u 1 S A ) P B ) ) ) = ( -u N x. 0 ) )
66 8 mul01d 
 |-  ( N e. NN0 -> ( -u N x. 0 ) = 0 )
67 65 66 sylan9eqr 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( -u N x. ( ( A P B ) + ( ( -u 1 S A ) P B ) ) ) = 0 )
68 53 67 eqtr3d 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N x. ( A P B ) ) + ( -u N x. ( ( -u 1 S A ) P B ) ) ) = 0 )
69 49 68 eqtr3d 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N x. ( A P B ) ) + -u ( N x. ( ( -u 1 S A ) P B ) ) ) = 0 )
70 40 46 69 3eqtr2d 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N x. ( A P B ) ) - ( ( -u N S A ) P B ) ) = 0 )
71 13 19 70 subeq0d 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( -u N x. ( A P B ) ) = ( ( -u N S A ) P B ) )
72 71 eqcomd 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( -u N S A ) P B ) = ( -u N x. ( A P B ) ) )