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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ipasslem1.b ⊢ 𝐵 ∈ 𝑋
Assertion ipasslem2 ( ( 𝑁 ∈ ℕ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 7 negcld ⊢ ( 𝑁 ∈ ℕ0 → - 𝑁 ∈ ℂ )
9 5 phnvi ⊢ 𝑈 ∈ NrmCVec
10 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
11 9 6 10 mp3an13 ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
12 mulcl ⊢ ( ( - 𝑁 ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ )
13 8 11 12 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ )
14 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 𝑆 𝐴 ) ∈ 𝑋 )
15 9 14 mp3an1 ⊢ ( ( - 𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 𝑆 𝐴 ) ∈ 𝑋 )
16 8 15 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 𝑆 𝐴 ) ∈ 𝑋 )
17 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 𝑁 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
18 9 6 17 mp3an13 ⊢ ( ( - 𝑁 𝑆 𝐴 ) ∈ 𝑋 → ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
19 16 18 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
20 ax-1cn ⊢ 1 ∈ ℂ
21 mulneg2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 · - 1 ) = - ( 𝑁 · 1 ) )
22 20 21 mpan2 ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 · - 1 ) = - ( 𝑁 · 1 ) )
23 mulid1 ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 · 1 ) = 𝑁 )
24 23 negeqd ⊢ ( 𝑁 ∈ ℂ → - ( 𝑁 · 1 ) = - 𝑁 )
25 22 24 eqtr2d ⊢ ( 𝑁 ∈ ℂ → - 𝑁 = ( 𝑁 · - 1 ) )
26 25 adantr ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → - 𝑁 = ( 𝑁 · - 1 ) )
27 26 oveq1d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 𝑆 𝐴 ) = ( ( 𝑁 · - 1 ) 𝑆 𝐴 ) )
28 neg1cn ⊢ - 1 ∈ ℂ
29 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑁 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑁 · - 1 ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( - 1 𝑆 𝐴 ) ) )
30 9 29 mpan ⊢ ( ( 𝑁 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · - 1 ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( - 1 𝑆 𝐴 ) ) )
31 28 30 mp3an2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · - 1 ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( - 1 𝑆 𝐴 ) ) )
32 27 31 eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 𝑆 𝐴 ) = ( 𝑁 𝑆 ( - 1 𝑆 𝐴 ) ) )
33 7 32 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 𝑆 𝐴 ) = ( 𝑁 𝑆 ( - 1 𝑆 𝐴 ) ) )
34 33 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑁 𝑆 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
35 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
36 9 28 35 mp3an12 ⊢ ( 𝐴 ∈ 𝑋 → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
37 1 2 3 4 5 6 ipasslem1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 𝑆 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
38 36 37 sylan2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
39 34 38 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
40 39 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) − ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) ) = ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) − ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) )
41 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
42 9 6 41 mp3an13 ⊢ ( ( - 1 𝑆 𝐴 ) ∈ 𝑋 → ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
43 36 42 syl ⊢ ( 𝐴 ∈ 𝑋 → ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
44 mulcl ⊢ ( ( 𝑁 ∈ ℂ ∧ ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ ) → ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ∈ ℂ )
45 7 43 44 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ∈ ℂ )
46 13 45 negsubd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) + - ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) = ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) − ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) )
47 mulneg1 ⊢ ( ( 𝑁 ∈ ℂ ∧ ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ ) → ( - 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) = - ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
48 7 43 47 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) = - ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
49 48 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) + ( - 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) = ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) + - ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) )
50 8 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → - 𝑁 ∈ ℂ )
51 11 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
52 43 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
53 50 51 52 adddid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 · ( ( 𝐴 𝑃 𝐵 ) + ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) = ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) + ( - 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) )
54 1 2 3 4 5 ipdiri ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( 𝐴 𝑃 𝐵 ) + ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
55 6 54 mp3an3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( 𝐴 𝑃 𝐵 ) + ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
56 36 55 mpdan ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( 𝐴 𝑃 𝐵 ) + ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
57 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
58 1 2 3 57 nvrinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) = ( 0vec ‘ 𝑈 ) )
59 9 58 mpan ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) = ( 0vec ‘ 𝑈 ) )
60 59 oveq1d ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) )
61 1 57 4 dip0l ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) = 0 )
62 9 6 61 mp2an ⊢ ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) = 0
63 60 62 eqtrdi ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = 0 )
64 56 63 eqtr3d ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝑃 𝐵 ) + ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) = 0 )
65 64 oveq2d ⊢ ( 𝐴 ∈ 𝑋 → ( - 𝑁 · ( ( 𝐴 𝑃 𝐵 ) + ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) = ( - 𝑁 · 0 ) )
66 8 mul01d ⊢ ( 𝑁 ∈ ℕ0 → ( - 𝑁 · 0 ) = 0 )
67 65 66 sylan9eqr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 · ( ( 𝐴 𝑃 𝐵 ) + ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) = 0 )
68 53 67 eqtr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) + ( - 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) = 0 )
69 49 68 eqtr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) + - ( 𝑁 · ( ( - 1 𝑆 𝐴 ) 𝑃 𝐵 ) ) ) = 0 )
70 40 46 69 3eqtr2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) − ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) ) = 0 )
71 13 19 70 subeq0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) = ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) )
72 71 eqcomd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )