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 = \cdot_{𝑠OLD} (U)$
	ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
	ipasslem1.b	$⊢ B \in X$
Assertion	ipasslem3	$⊢ (N \in ℤ \land A \in X) \to (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 = \cdot_{𝑠OLD} (U)$
4		ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
5		ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
6		ipasslem1.b	$⊢ B \in X$
7		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
8	1 2 3 4 5 6	ipasslem1	$⊢ (N \in ℕ_{0} \land A \in X) \to (N S A) P B = N (A P B)$
9		nnnn0	$⊢ - N \in ℕ \to - N \in ℕ_{0}$
10	1 2 3 4 5 6	ipasslem2	$⊢ (- N \in ℕ_{0} \land A \in X) \to ((- -N) S A) P B = (- -N) (A P B)$
11	9 10	sylan	$⊢ (- N \in ℕ \land A \in X) \to ((- -N) S A) P B = (- -N) (A P B)$
12	11	adantll	$⊢ ((N \in ℝ \land - N \in ℕ) \land A \in X) \to ((- -N) S A) P B = (- -N) (A P B)$
13		recn	$⊢ N \in ℝ \to N \in ℂ$
14	13	negnegd	$⊢ N \in ℝ \to - -N = N$
15	14	oveq1d	$⊢ N \in ℝ \to (- -N) S A = N S A$
16	15	oveq1d	$⊢ N \in ℝ \to ((- -N) S A) P B = (N S A) P B$
17	16	ad2antrr	$⊢ ((N \in ℝ \land - N \in ℕ) \land A \in X) \to ((- -N) S A) P B = (N S A) P B$
18	14	oveq1d	$⊢ N \in ℝ \to (- -N) (A P B) = N (A P B)$
19	18	ad2antrr	$⊢ ((N \in ℝ \land - N \in ℕ) \land A \in X) \to (- -N) (A P B) = N (A P B)$
20	12 17 19	3eqtr3d	$⊢ ((N \in ℝ \land - N \in ℕ) \land A \in X) \to (N S A) P B = N (A P B)$
21	8 20	jaoian	$⊢ ((N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ)) \land A \in X) \to (N S A) P B = N (A P B)$
22	7 21	sylanb	$⊢ (N \in ℤ \land A \in X) \to (N S A) P B = N (A P B)$

Metamath Proof Explorer

Theorem ipasslem3

Proof