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	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )