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 = ⋅ 𝑠OLD ⁡ U
ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip1i.9 ⊢ U ∈ CPreHil OLD
ipasslem1.b ⊢ B ∈ X
Assertion ipasslem3 ⊢ N ∈ ℤ ∧ A ∈ X → N S A P B = N ⁢ A P B

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ X = BaseSet ⁡ U
2 ip1i.2 ⊢ G = + v ⁡ U
3 ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
5 ip1i.9 ⊢ U ∈ CPreHil OLD
6 ipasslem1.b ⊢ B ∈ X
7 elznn0nn ⊢ N ∈ ℤ ↔ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ − N ∈ ℕ
8 1 2 3 4 5 6 ipasslem1 ⊢ N ∈ ℕ 0 ∧ A ∈ X → N S A P B = N ⁢ A P B
9 nnnn0 ⊢ − N ∈ ℕ → − N ∈ ℕ 0
10 1 2 3 4 5 6 ipasslem2 ⊢ − N ∈ ℕ 0 ∧ A ∈ X → − -N S A P B = − -N ⁢ A P B
11 9 10 sylan ⊢ − N ∈ ℕ ∧ A ∈ X → − -N S A P B = − -N ⁢ A P B
12 11 adantll ⊢ N ∈ ℝ ∧ − N ∈ ℕ ∧ A ∈ X → − -N S A P B = − -N ⁢ A P B
13 recn ⊢ N ∈ ℝ → N ∈ ℂ
14 13 negnegd ⊢ N ∈ ℝ → − -N = N
15 14 oveq1d ⊢ N ∈ ℝ → − -N S A = N S A
16 15 oveq1d ⊢ N ∈ ℝ → − -N S A P B = N S A P B
17 16 ad2antrr ⊢ N ∈ ℝ ∧ − N ∈ ℕ ∧ A ∈ X → − -N S A P B = N S A P B
18 14 oveq1d ⊢ N ∈ ℝ → − -N ⁢ A P B = N ⁢ A P B
19 18 ad2antrr ⊢ N ∈ ℝ ∧ − N ∈ ℕ ∧ A ∈ X → − -N ⁢ A P B = N ⁢ A P B
20 12 17 19 3eqtr3d ⊢ N ∈ ℝ ∧ − N ∈ ℕ ∧ A ∈ X → N S A P B = N ⁢ A P B
21 8 20 jaoian ⊢ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ − N ∈ ℕ ∧ A ∈ X → N S A P B = N ⁢ A P B
22 7 21 sylanb ⊢ N ∈ ℤ ∧ A ∈ X → N S A P B = N ⁢ A P B