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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ipasslem1.b ⊢ 𝐵 ∈ 𝑋
Assertion ipasslem1 ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
5 ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
6 ipasslem1.b ⊢ 𝐵 ∈ 𝑋
7 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
8 ax-1cn ⊢ 1 ∈ ℂ
9 5 phnvi ⊢ 𝑈 ∈ NrmCVec
10 1 2 3 nvdir ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
11 9 10 mpan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
12 8 11 mp3an2 ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
13 7 12 sylan ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
14 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
15 9 14 mpan ⊢ ( 𝐴 ∈ 𝑋 → ( 1 𝑆 𝐴 ) = 𝐴 )
16 15 adantl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
17 16 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) )
18 13 17 eqtrd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) )
19 18 oveq1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) )
20 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
21 9 6 20 mp3an13 ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
22 21 mullidd ⊢ ( 𝐴 ∈ 𝑋 → ( 1 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐴 𝑃 𝐵 ) )
23 22 adantl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( 1 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐴 𝑃 𝐵 ) )
24 23 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 𝐴 𝑃 𝐵 ) ) )
25 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 )
26 9 25 mp3an1 ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 )
27 7 26 sylan ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 )
28 1 2 3 4 5 ipdiri ⊢ ( ( ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 𝐴 𝑃 𝐵 ) ) )
29 6 28 mp3an3 ⊢ ( ( ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 𝐴 𝑃 𝐵 ) ) )
30 27 29 sylancom ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 𝐴 𝑃 𝐵 ) ) )
31 24 30 eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) )
32 19 31 eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
33 oveq1 ⊢ ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
34 32 33 sylan9eq ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
35 adddir ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
36 8 35 mp3an2 ⊢ ( ( 𝑘 ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
37 7 21 36 syl2an ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
38 37 adantr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
39 34 38 eqtr4d ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) )
40 39 exp31 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐴 ∈ 𝑋 → ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) ) ) )
41 40 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) → ( 𝐴 ∈ 𝑋 → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) ) ) )
42 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
43 1 42 4 dip0l ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) = 0 )
44 9 6 43 mp2an ⊢ ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) = 0
45 1 3 42 nv0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 0 𝑆 𝐴 ) = ( 0vec ‘ 𝑈 ) )
46 9 45 mpan ⊢ ( 𝐴 ∈ 𝑋 → ( 0 𝑆 𝐴 ) = ( 0vec ‘ 𝑈 ) )
47 46 oveq1d ⊢ ( 𝐴 ∈ 𝑋 → ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) )
48 21 mul02d ⊢ ( 𝐴 ∈ 𝑋 → ( 0 · ( 𝐴 𝑃 𝐵 ) ) = 0 )
49 44 47 48 3eqtr4a ⊢ ( 𝐴 ∈ 𝑋 → ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 0 · ( 𝐴 𝑃 𝐵 ) ) )
50 oveq1 ⊢ ( 𝑗 = 0 → ( 𝑗 𝑆 𝐴 ) = ( 0 𝑆 𝐴 ) )
51 50 oveq1d ⊢ ( 𝑗 = 0 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) )
52 oveq1 ⊢ ( 𝑗 = 0 → ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) = ( 0 · ( 𝐴 𝑃 𝐵 ) ) )
53 51 52 eqeq12d ⊢ ( 𝑗 = 0 → ( ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 0 · ( 𝐴 𝑃 𝐵 ) ) ) )
54 53 imbi2d ⊢ ( 𝑗 = 0 → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 0 · ( 𝐴 𝑃 𝐵 ) ) ) ) )
55 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 𝑆 𝐴 ) = ( 𝑘 𝑆 𝐴 ) )
56 55 oveq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) )
57 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) )
58 56 57 eqeq12d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) )
59 58 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) ) )
60 oveq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 𝑆 𝐴 ) = ( ( 𝑘 + 1 ) 𝑆 𝐴 ) )
61 60 oveq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) )
62 oveq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) )
63 61 62 eqeq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
64 63 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) ) ) )
65 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 𝑆 𝐴 ) = ( 𝑁 𝑆 𝐴 ) )
66 65 oveq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) )
67 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
68 66 67 eqeq12d ⊢ ( 𝑗 = 𝑁 → ( ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) ) )
69 68 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) ) ) )
70 41 49 54 59 64 69 nn0indALT ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ 𝑋 → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) ) )
71 70 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )