This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( .sOLD ` U )
ip1i.7 
|- P = ( .iOLD ` U )
ip1i.9 
|- U e. CPreHilOLD
ipasslem1.b 
|- B e. X
Assertion ipasslem3 
|- ( ( N e. ZZ /\ A e. X ) -> ( ( N S A ) P B ) = ( 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 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
8 1 2 3 4 5 6 ipasslem1 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )
9 nnnn0 
 |-  ( -u N e. NN -> -u N e. NN0 )
10 1 2 3 4 5 6 ipasslem2 
 |-  ( ( -u N e. NN0 /\ A e. X ) -> ( ( -u -u N S A ) P B ) = ( -u -u N x. ( A P B ) ) )
11 9 10 sylan 
 |-  ( ( -u N e. NN /\ A e. X ) -> ( ( -u -u N S A ) P B ) = ( -u -u N x. ( A P B ) ) )
12 11 adantll 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ A e. X ) -> ( ( -u -u N S A ) P B ) = ( -u -u N x. ( A P B ) ) )
13 recn 
 |-  ( N e. RR -> N e. CC )
14 13 negnegd 
 |-  ( N e. RR -> -u -u N = N )
15 14 oveq1d 
 |-  ( N e. RR -> ( -u -u N S A ) = ( N S A ) )
16 15 oveq1d 
 |-  ( N e. RR -> ( ( -u -u N S A ) P B ) = ( ( N S A ) P B ) )
17 16 ad2antrr 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ A e. X ) -> ( ( -u -u N S A ) P B ) = ( ( N S A ) P B ) )
18 14 oveq1d 
 |-  ( N e. RR -> ( -u -u N x. ( A P B ) ) = ( N x. ( A P B ) ) )
19 18 ad2antrr 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ A e. X ) -> ( -u -u N x. ( A P B ) ) = ( N x. ( A P B ) ) )
20 12 17 19 3eqtr3d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )
21 8 20 jaoian 
 |-  ( ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )
22 7 21 sylanb 
 |-  ( ( N e. ZZ /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )