Metamath Proof Explorer

Theorem ipasslem1

Description: Lemma for ipassi . Show the inner product associative law for nonnegative 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 ipasslem1 
|- ( ( N e. NN0 /\ 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 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
8 ax-1cn 
 |-  1 e. CC
9 5 phnvi 
 |-  U e. NrmCVec
10 1 2 3 nvdir 
 |-  ( ( U e. NrmCVec /\ ( k e. CC /\ 1 e. CC /\ A e. X ) ) -> ( ( k + 1 ) S A ) = ( ( k S A ) G ( 1 S A ) ) )
11 9 10 mpan 
 |-  ( ( k e. CC /\ 1 e. CC /\ A e. X ) -> ( ( k + 1 ) S A ) = ( ( k S A ) G ( 1 S A ) ) )
12 8 11 mp3an2 
 |-  ( ( k e. CC /\ A e. X ) -> ( ( k + 1 ) S A ) = ( ( k S A ) G ( 1 S A ) ) )
13 7 12 sylan 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( k + 1 ) S A ) = ( ( k S A ) G ( 1 S A ) ) )
14 1 3 nvsid 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 S A ) = A )
15 9 14 mpan 
 |-  ( A e. X -> ( 1 S A ) = A )
16 15 adantl 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( 1 S A ) = A )
17 16 oveq2d 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( k S A ) G ( 1 S A ) ) = ( ( k S A ) G A ) )
18 13 17 eqtrd 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( k + 1 ) S A ) = ( ( k S A ) G A ) )
19 18 oveq1d 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( ( k + 1 ) S A ) P B ) = ( ( ( k S A ) G A ) P B ) )
20 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
21 9 6 20 mp3an13 
 |-  ( A e. X -> ( A P B ) e. CC )
22 21 mulid2d 
 |-  ( A e. X -> ( 1 x. ( A P B ) ) = ( A P B ) )
23 22 adantl 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( 1 x. ( A P B ) ) = ( A P B ) )
24 23 oveq2d 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( ( k S A ) P B ) + ( 1 x. ( A P B ) ) ) = ( ( ( k S A ) P B ) + ( A P B ) ) )
25 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ k e. CC /\ A e. X ) -> ( k S A ) e. X )
26 9 25 mp3an1 
 |-  ( ( k e. CC /\ A e. X ) -> ( k S A ) e. X )
27 7 26 sylan 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( k S A ) e. X )
28 1 2 3 4 5 ipdiri 
 |-  ( ( ( k S A ) e. X /\ A e. X /\ B e. X ) -> ( ( ( k S A ) G A ) P B ) = ( ( ( k S A ) P B ) + ( A P B ) ) )
29 6 28 mp3an3 
 |-  ( ( ( k S A ) e. X /\ A e. X ) -> ( ( ( k S A ) G A ) P B ) = ( ( ( k S A ) P B ) + ( A P B ) ) )
30 27 29 sylancom 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( ( k S A ) G A ) P B ) = ( ( ( k S A ) P B ) + ( A P B ) ) )
31 24 30 eqtr4d 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( ( k S A ) P B ) + ( 1 x. ( A P B ) ) ) = ( ( ( k S A ) G A ) P B ) )
32 19 31 eqtr4d 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( ( k + 1 ) S A ) P B ) = ( ( ( k S A ) P B ) + ( 1 x. ( A P B ) ) ) )
33 oveq1 
 |-  ( ( ( k S A ) P B ) = ( k x. ( A P B ) ) -> ( ( ( k S A ) P B ) + ( 1 x. ( A P B ) ) ) = ( ( k x. ( A P B ) ) + ( 1 x. ( A P B ) ) ) )
34 32 33 sylan9eq 
 |-  ( ( ( k e. NN0 /\ A e. X ) /\ ( ( k S A ) P B ) = ( k x. ( A P B ) ) ) -> ( ( ( k + 1 ) S A ) P B ) = ( ( k x. ( A P B ) ) + ( 1 x. ( A P B ) ) ) )
35 adddir 
 |-  ( ( k e. CC /\ 1 e. CC /\ ( A P B ) e. CC ) -> ( ( k + 1 ) x. ( A P B ) ) = ( ( k x. ( A P B ) ) + ( 1 x. ( A P B ) ) ) )
36 8 35 mp3an2 
 |-  ( ( k e. CC /\ ( A P B ) e. CC ) -> ( ( k + 1 ) x. ( A P B ) ) = ( ( k x. ( A P B ) ) + ( 1 x. ( A P B ) ) ) )
37 7 21 36 syl2an 
 |-  ( ( k e. NN0 /\ A e. X ) -> ( ( k + 1 ) x. ( A P B ) ) = ( ( k x. ( A P B ) ) + ( 1 x. ( A P B ) ) ) )
38 37 adantr 
 |-  ( ( ( k e. NN0 /\ A e. X ) /\ ( ( k S A ) P B ) = ( k x. ( A P B ) ) ) -> ( ( k + 1 ) x. ( A P B ) ) = ( ( k x. ( A P B ) ) + ( 1 x. ( A P B ) ) ) )
39 34 38 eqtr4d 
 |-  ( ( ( k e. NN0 /\ A e. X ) /\ ( ( k S A ) P B ) = ( k x. ( A P B ) ) ) -> ( ( ( k + 1 ) S A ) P B ) = ( ( k + 1 ) x. ( A P B ) ) )
40 39 exp31 
 |-  ( k e. NN0 -> ( A e. X -> ( ( ( k S A ) P B ) = ( k x. ( A P B ) ) -> ( ( ( k + 1 ) S A ) P B ) = ( ( k + 1 ) x. ( A P B ) ) ) ) )
41 40 a2d 
 |-  ( k e. NN0 -> ( ( A e. X -> ( ( k S A ) P B ) = ( k x. ( A P B ) ) ) -> ( A e. X -> ( ( ( k + 1 ) S A ) P B ) = ( ( k + 1 ) x. ( A P B ) ) ) ) )
42 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
43 1 42 4 dip0l 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( ( 0vec ` U ) P B ) = 0 )
44 9 6 43 mp2an 
 |-  ( ( 0vec ` U ) P B ) = 0
45 1 3 42 nv0 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 0 S A ) = ( 0vec ` U ) )
46 9 45 mpan 
 |-  ( A e. X -> ( 0 S A ) = ( 0vec ` U ) )
47 46 oveq1d 
 |-  ( A e. X -> ( ( 0 S A ) P B ) = ( ( 0vec ` U ) P B ) )
48 21 mul02d 
 |-  ( A e. X -> ( 0 x. ( A P B ) ) = 0 )
49 44 47 48 3eqtr4a 
 |-  ( A e. X -> ( ( 0 S A ) P B ) = ( 0 x. ( A P B ) ) )
50 oveq1 
 |-  ( j = 0 -> ( j S A ) = ( 0 S A ) )
51 50 oveq1d 
 |-  ( j = 0 -> ( ( j S A ) P B ) = ( ( 0 S A ) P B ) )
52 oveq1 
 |-  ( j = 0 -> ( j x. ( A P B ) ) = ( 0 x. ( A P B ) ) )
53 51 52 eqeq12d 
 |-  ( j = 0 -> ( ( ( j S A ) P B ) = ( j x. ( A P B ) ) <-> ( ( 0 S A ) P B ) = ( 0 x. ( A P B ) ) ) )
54 53 imbi2d 
 |-  ( j = 0 -> ( ( A e. X -> ( ( j S A ) P B ) = ( j x. ( A P B ) ) ) <-> ( A e. X -> ( ( 0 S A ) P B ) = ( 0 x. ( A P B ) ) ) ) )
55 oveq1 
 |-  ( j = k -> ( j S A ) = ( k S A ) )
56 55 oveq1d 
 |-  ( j = k -> ( ( j S A ) P B ) = ( ( k S A ) P B ) )
57 oveq1 
 |-  ( j = k -> ( j x. ( A P B ) ) = ( k x. ( A P B ) ) )
58 56 57 eqeq12d 
 |-  ( j = k -> ( ( ( j S A ) P B ) = ( j x. ( A P B ) ) <-> ( ( k S A ) P B ) = ( k x. ( A P B ) ) ) )
59 58 imbi2d 
 |-  ( j = k -> ( ( A e. X -> ( ( j S A ) P B ) = ( j x. ( A P B ) ) ) <-> ( A e. X -> ( ( k S A ) P B ) = ( k x. ( A P B ) ) ) ) )
60 oveq1 
 |-  ( j = ( k + 1 ) -> ( j S A ) = ( ( k + 1 ) S A ) )
61 60 oveq1d 
 |-  ( j = ( k + 1 ) -> ( ( j S A ) P B ) = ( ( ( k + 1 ) S A ) P B ) )
62 oveq1 
 |-  ( j = ( k + 1 ) -> ( j x. ( A P B ) ) = ( ( k + 1 ) x. ( A P B ) ) )
63 61 62 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( ( ( j S A ) P B ) = ( j x. ( A P B ) ) <-> ( ( ( k + 1 ) S A ) P B ) = ( ( k + 1 ) x. ( A P B ) ) ) )
64 63 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( A e. X -> ( ( j S A ) P B ) = ( j x. ( A P B ) ) ) <-> ( A e. X -> ( ( ( k + 1 ) S A ) P B ) = ( ( k + 1 ) x. ( A P B ) ) ) ) )
65 oveq1 
 |-  ( j = N -> ( j S A ) = ( N S A ) )
66 65 oveq1d 
 |-  ( j = N -> ( ( j S A ) P B ) = ( ( N S A ) P B ) )
67 oveq1 
 |-  ( j = N -> ( j x. ( A P B ) ) = ( N x. ( A P B ) ) )
68 66 67 eqeq12d 
 |-  ( j = N -> ( ( ( j S A ) P B ) = ( j x. ( A P B ) ) <-> ( ( N S A ) P B ) = ( N x. ( A P B ) ) ) )
69 68 imbi2d 
 |-  ( j = N -> ( ( A e. X -> ( ( j S A ) P B ) = ( j x. ( A P B ) ) ) <-> ( A e. X -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) ) ) )
70 41 49 54 59 64 69 nn0indALT 
 |-  ( N e. NN0 -> ( A e. X -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) ) )
71 70 imp 
 |-  ( ( N e. NN0 /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )