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 = 𝑠OLD U
ip1i.7 P = 𝑖OLD U
ip1i.9 U CPreHil OLD
ipasslem1.b B X
Assertion ipasslem2 N 0 A X -N S A P B = -N A P B

Proof

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