ipasslem2

Description: Lemma for ipassi . Show the inner product associative law for nonpositive 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	ipasslem2	$⊢ (N \in ℕ_{0} \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		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
8	7	negcld	$⊢ N \in ℕ_{0} \to - N \in ℂ$
9	5	phnvi	$⊢ U \in NrmCVec$
10	1 4	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
11	9 6 10	mp3an13	$⊢ A \in X \to A P B \in ℂ$
12		mulcl	$⊢ (- N \in ℂ \land A P B \in ℂ) \to -N (A P B) \in ℂ$
13	8 11 12	syl2an	$⊢ (N \in ℕ_{0} \land A \in X) \to -N (A P B) \in ℂ$
14	1 3	nvscl	$⊢ (U \in NrmCVec \land - N \in ℂ \land A \in X) \to -N S A \in X$
15	9 14	mp3an1	$⊢ (- N \in ℂ \land A \in X) \to -N S A \in X$
16	8 15	sylan	$⊢ (N \in ℕ_{0} \land A \in X) \to -N S A \in X$
17	1 4	dipcl	$⊢ (U \in NrmCVec \land -N S A \in X \land B \in X) \to (-N S A) P B \in ℂ$
18	9 6 17	mp3an13	$⊢ -N S A \in X \to (-N S A) P B \in ℂ$
19	16 18	syl	$⊢ (N \in ℕ_{0} \land A \in X) \to (-N S A) P B \in ℂ$
20		ax-1cn	$⊢ 1 \in ℂ$
21		mulneg2	$⊢ (N \in ℂ \land 1 \in ℂ) \to N -1 = - N \cdot 1$
22	20 21	mpan2	$⊢ N \in ℂ \to N -1 = - N \cdot 1$
23		mulrid	$⊢ N \in ℂ \to N \cdot 1 = N$
24	23	negeqd	$⊢ N \in ℂ \to - N \cdot 1 = - N$
25	22 24	eqtr2d	$⊢ N \in ℂ \to - N = N -1$
26	25	adantr	$⊢ (N \in ℂ \land A \in X) \to - N = N -1$
27	26	oveq1d	$⊢ (N \in ℂ \land A \in X) \to -N S A = N -1 S A$
28		neg1cn	$⊢ - 1 \in ℂ$
29	1 3	nvsass	$⊢ (U \in NrmCVec \land (N \in ℂ \land - 1 \in ℂ \land A \in X)) \to N -1 S A = N S (-1 S A)$
30	9 29	mpan	$⊢ (N \in ℂ \land - 1 \in ℂ \land A \in X) \to N -1 S A = N S (-1 S A)$
31	28 30	mp3an2	$⊢ (N \in ℂ \land A \in X) \to N -1 S A = N S (-1 S A)$
32	27 31	eqtrd	$⊢ (N \in ℂ \land A \in X) \to -N S A = N S (-1 S A)$
33	7 32	sylan	$⊢ (N \in ℕ_{0} \land A \in X) \to -N S A = N S (-1 S A)$
34	33	oveq1d	$⊢ (N \in ℕ_{0} \land A \in X) \to (-N S A) P B = (N S (-1 S A)) P B$
35	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land A \in X) \to -1 S A \in X$
36	9 28 35	mp3an12	$⊢ A \in X \to -1 S A \in X$
37	1 2 3 4 5 6	ipasslem1	$⊢ (N \in ℕ_{0} \land -1 S A \in X) \to (N S (-1 S A)) P B = N ((-1 S A) P B)$
38	36 37	sylan2	$⊢ (N \in ℕ_{0} \land A \in X) \to (N S (-1 S A)) P B = N ((-1 S A) P B)$
39	34 38	eqtrd	$⊢ (N \in ℕ_{0} \land A \in X) \to (-N S A) P B = N ((-1 S A) P B)$
40	39	oveq2d	$⊢ (N \in ℕ_{0} \land A \in X) \to -N (A P B) - ((-N S A) P B) = -N (A P B) - N ((-1 S A) P B)$
41	1 4	dipcl	$⊢ (U \in NrmCVec \land -1 S A \in X \land B \in X) \to (-1 S A) P B \in ℂ$
42	9 6 41	mp3an13	$⊢ -1 S A \in X \to (-1 S A) P B \in ℂ$
43	36 42	syl	$⊢ A \in X \to (-1 S A) P B \in ℂ$
44		mulcl	$⊢ (N \in ℂ \land (-1 S A) P B \in ℂ) \to N ((-1 S A) P B) \in ℂ$
45	7 43 44	syl2an	$⊢ (N \in ℕ_{0} \land A \in X) \to N ((-1 S A) P B) \in ℂ$
46	13 45	negsubd	$⊢ (N \in ℕ_{0} \land A \in X) \to -N (A P B) + (- N ((-1 S A) P B)) = -N (A P B) - N ((-1 S A) P B)$
47		mulneg1	$⊢ (N \in ℂ \land (-1 S A) P B \in ℂ) \to -N ((-1 S A) P B) = - N ((-1 S A) P B)$
48	7 43 47	syl2an	$⊢ (N \in ℕ_{0} \land A \in X) \to -N ((-1 S A) P B) = - N ((-1 S A) P B)$
49	48	oveq2d	$⊢ (N \in ℕ_{0} \land A \in X) \to -N (A P B) + -N ((-1 S A) P B) = -N (A P B) + (- N ((-1 S A) P B))$
50	8	adantr	$⊢ (N \in ℕ_{0} \land A \in X) \to - N \in ℂ$
51	11	adantl	$⊢ (N \in ℕ_{0} \land A \in X) \to A P B \in ℂ$
52	43	adantl	$⊢ (N \in ℕ_{0} \land A \in X) \to (-1 S A) P B \in ℂ$
53	50 51 52	adddid	$⊢ (N \in ℕ_{0} \land A \in X) \to -N ((A P B) + ((-1 S A) P B)) = -N (A P B) + -N ((-1 S A) P B)$
54	1 2 3 4 5	ipdiri	$⊢ (A \in X \land -1 S A \in X \land B \in X) \to (A G (-1 S A)) P B = (A P B) + ((-1 S A) P B)$
55	6 54	mp3an3	$⊢ (A \in X \land -1 S A \in X) \to (A G (-1 S A)) P B = (A P B) + ((-1 S A) P B)$
56	36 55	mpdan	$⊢ A \in X \to (A G (-1 S A)) P B = (A P B) + ((-1 S A) P B)$
57		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
58	1 2 3 57	nvrinv	$⊢ (U \in NrmCVec \land A \in X) \to A G (-1 S A) = 0_{vec} (U)$
59	9 58	mpan	$⊢ A \in X \to A G (-1 S A) = 0_{vec} (U)$
60	59	oveq1d	$⊢ A \in X \to (A G (-1 S A)) P B = 0_{vec} (U) P B$
61	1 57 4	dip0l	$⊢ (U \in NrmCVec \land B \in X) \to 0_{vec} (U) P B = 0$
62	9 6 61	mp2an	$⊢ 0_{vec} (U) P B = 0$
63	60 62	eqtrdi	$⊢ A \in X \to (A G (-1 S A)) P B = 0$
64	56 63	eqtr3d	$⊢ A \in X \to (A P B) + ((-1 S A) P B) = 0$
65	64	oveq2d	$⊢ A \in X \to -N ((A P B) + ((-1 S A) P B)) = -N \cdot 0$
66	8	mul01d	$⊢ N \in ℕ_{0} \to -N \cdot 0 = 0$
67	65 66	sylan9eqr	$⊢ (N \in ℕ_{0} \land A \in X) \to -N ((A P B) + ((-1 S A) P B)) = 0$
68	53 67	eqtr3d	$⊢ (N \in ℕ_{0} \land A \in X) \to -N (A P B) + -N ((-1 S A) P B) = 0$
69	49 68	eqtr3d	$⊢ (N \in ℕ_{0} \land A \in X) \to -N (A P B) + (- N ((-1 S A) P B)) = 0$
70	40 46 69	3eqtr2d	$⊢ (N \in ℕ_{0} \land A \in X) \to -N (A P B) - ((-N S A) P B) = 0$
71	13 19 70	subeq0d	$⊢ (N \in ℕ_{0} \land A \in X) \to -N (A P B) = (-N S A) P B$
72	71	eqcomd	$⊢ (N \in ℕ_{0} \land A \in X) \to (-N S A) P B = -N (A P B)$

Metamath Proof Explorer

Theorem ipasslem2

Proof