ipasslem4

Description: Lemma for ipassi . Show the inner product associative law for positive integer reciprocals. (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	ipasslem4	$⊢ (N \in ℕ \land A \in X) \to ((\frac{1}{N}) S A) P B = (\frac{1}{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		nnrecre	$⊢ N \in ℕ \to \frac{1}{N} \in ℝ$
8	7	recnd	$⊢ N \in ℕ \to \frac{1}{N} \in ℂ$
9	5	phnvi	$⊢ U \in NrmCVec$
10	1 3	nvscl	$⊢ (U \in NrmCVec \land \frac{1}{N} \in ℂ \land A \in X) \to (\frac{1}{N}) S A \in X$
11	9 10	mp3an1	$⊢ (\frac{1}{N} \in ℂ \land A \in X) \to (\frac{1}{N}) S A \in X$
12	8 11	sylan	$⊢ (N \in ℕ \land A \in X) \to (\frac{1}{N}) S A \in X$
13	1 4	dipcl	$⊢ (U \in NrmCVec \land (\frac{1}{N}) S A \in X \land B \in X) \to ((\frac{1}{N}) S A) P B \in ℂ$
14	9 6 13	mp3an13	$⊢ (\frac{1}{N}) S A \in X \to ((\frac{1}{N}) S A) P B \in ℂ$
15	12 14	syl	$⊢ (N \in ℕ \land A \in X) \to ((\frac{1}{N}) S A) P B \in ℂ$
16	1 4	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
17	9 6 16	mp3an13	$⊢ A \in X \to A P B \in ℂ$
18		mulcl	$⊢ (\frac{1}{N} \in ℂ \land A P B \in ℂ) \to (\frac{1}{N}) (A P B) \in ℂ$
19	8 17 18	syl2an	$⊢ (N \in ℕ \land A \in X) \to (\frac{1}{N}) (A P B) \in ℂ$
20		nncn	$⊢ N \in ℕ \to N \in ℂ$
21	20	adantr	$⊢ (N \in ℕ \land A \in X) \to N \in ℂ$
22		nnne0	$⊢ N \in ℕ \to N \neq 0$
23	22	adantr	$⊢ (N \in ℕ \land A \in X) \to N \neq 0$
24	20 22	recidd	$⊢ N \in ℕ \to N (\frac{1}{N}) = 1$
25	24	oveq1d	$⊢ N \in ℕ \to N (\frac{1}{N}) (A P B) = 1 (A P B)$
26	17	mullidd	$⊢ A \in X \to 1 (A P B) = A P B$
27	25 26	sylan9eq	$⊢ (N \in ℕ \land A \in X) \to N (\frac{1}{N}) (A P B) = A P B$
28	24	oveq1d	$⊢ N \in ℕ \to N (\frac{1}{N}) S A = 1 S A$
29	1 3	nvsid	$⊢ (U \in NrmCVec \land A \in X) \to 1 S A = A$
30	9 29	mpan	$⊢ A \in X \to 1 S A = A$
31	28 30	sylan9eq	$⊢ (N \in ℕ \land A \in X) \to N (\frac{1}{N}) S A = A$
32	8	adantr	$⊢ (N \in ℕ \land A \in X) \to \frac{1}{N} \in ℂ$
33		simpr	$⊢ (N \in ℕ \land A \in X) \to A \in X$
34	1 3	nvsass	$⊢ (U \in NrmCVec \land (N \in ℂ \land \frac{1}{N} \in ℂ \land A \in X)) \to N (\frac{1}{N}) S A = N S ((\frac{1}{N}) S A)$
35	9 34	mpan	$⊢ (N \in ℂ \land \frac{1}{N} \in ℂ \land A \in X) \to N (\frac{1}{N}) S A = N S ((\frac{1}{N}) S A)$
36	21 32 33 35	syl3anc	$⊢ (N \in ℕ \land A \in X) \to N (\frac{1}{N}) S A = N S ((\frac{1}{N}) S A)$
37	31 36	eqtr3d	$⊢ (N \in ℕ \land A \in X) \to A = N S ((\frac{1}{N}) S A)$
38	37	oveq1d	$⊢ (N \in ℕ \land A \in X) \to A P B = (N S ((\frac{1}{N}) S A)) P B$
39		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
40	39	adantr	$⊢ (N \in ℕ \land A \in X) \to N \in ℕ_{0}$
41	1 2 3 4 5 6	ipasslem1	$⊢ (N \in ℕ_{0} \land (\frac{1}{N}) S A \in X) \to (N S ((\frac{1}{N}) S A)) P B = N (((\frac{1}{N}) S A) P B)$
42	40 12 41	syl2anc	$⊢ (N \in ℕ \land A \in X) \to (N S ((\frac{1}{N}) S A)) P B = N (((\frac{1}{N}) S A) P B)$
43	27 38 42	3eqtrd	$⊢ (N \in ℕ \land A \in X) \to N (\frac{1}{N}) (A P B) = N (((\frac{1}{N}) S A) P B)$
44	17	adantl	$⊢ (N \in ℕ \land A \in X) \to A P B \in ℂ$
45	21 32 44	mulassd	$⊢ (N \in ℕ \land A \in X) \to N (\frac{1}{N}) (A P B) = N (\frac{1}{N}) (A P B)$
46	43 45	eqtr3d	$⊢ (N \in ℕ \land A \in X) \to N (((\frac{1}{N}) S A) P B) = N (\frac{1}{N}) (A P B)$
47	15 19 21 23 46	mulcanad	$⊢ (N \in ℕ \land A \in X) \to ((\frac{1}{N}) S A) P B = (\frac{1}{N}) (A P B)$

Metamath Proof Explorer

Theorem ipasslem4

Proof