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

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 elznn0nn ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
8 1 2 3 4 5 6 ipasslem1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
9 nnnn0 ⊢ ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℕ0 )
10 1 2 3 4 5 6 ipasslem2 ⊢ ( ( - 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( - - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( - - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
11 9 10 sylan ⊢ ( ( - 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( - - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( - - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
12 11 adantll ⊢ ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝐴 ∈ 𝑋 ) → ( ( - - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( - - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
13 recn ⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
14 13 negnegd ⊢ ( 𝑁 ∈ ℝ → - - 𝑁 = 𝑁 )
15 14 oveq1d ⊢ ( 𝑁 ∈ ℝ → ( - - 𝑁 𝑆 𝐴 ) = ( 𝑁 𝑆 𝐴 ) )
16 15 oveq1d ⊢ ( 𝑁 ∈ ℝ → ( ( - - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) )
17 16 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝐴 ∈ 𝑋 ) → ( ( - - 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) )
18 14 oveq1d ⊢ ( 𝑁 ∈ ℝ → ( - - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
19 18 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝐴 ∈ 𝑋 ) → ( - - 𝑁 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
20 12 17 19 3eqtr3d ⊢ ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
21 8 20 jaoian ⊢ ( ( ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
22 7 21 sylanb ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )