Metamath Proof Explorer


Theorem ipasslem3

Description: Lemma for ipassi . Show the inner product associative law for all 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 ipasslem3 N 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 elznn0nn N N 0 N N
8 1 2 3 4 5 6 ipasslem1 N 0 A X N S A P B = N A P B
9 nnnn0 N N 0
10 1 2 3 4 5 6 ipasslem2 N 0 A X -N S A P B = -N A P B
11 9 10 sylan N A X -N S A P B = -N A P B
12 11 adantll N N A X -N S A P B = -N A P B
13 recn N N
14 13 negnegd N -N = N
15 14 oveq1d N -N S A = N S A
16 15 oveq1d N -N S A P B = N S A P B
17 16 ad2antrr N N A X -N S A P B = N S A P B
18 14 oveq1d N -N A P B = N A P B
19 18 ad2antrr N N A X -N A P B = N A P B
20 12 17 19 3eqtr3d N N A X N S A P B = N A P B
21 8 20 jaoian N 0 N N A X N S A P B = N A P B
22 7 21 sylanb N A X N S A P B = N A P B