ipasslem1

Description: Lemma for ipassi . Show the inner product associative law for nonnegative 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	ipasslem1	$⊢ (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	$⊢ k \in ℕ_{0} \to k \in ℂ$
8		ax-1cn	$⊢ 1 \in ℂ$
9	5	phnvi	$⊢ U \in NrmCVec$
10	1 2 3	nvdir	$⊢ (U \in NrmCVec \land (k \in ℂ \land 1 \in ℂ \land A \in X)) \to (k + 1) S A = (k S A) G (1 S A)$
11	9 10	mpan	$⊢ (k \in ℂ \land 1 \in ℂ \land A \in X) \to (k + 1) S A = (k S A) G (1 S A)$
12	8 11	mp3an2	$⊢ (k \in ℂ \land A \in X) \to (k + 1) S A = (k S A) G (1 S A)$
13	7 12	sylan	$⊢ (k \in ℕ_{0} \land A \in X) \to (k + 1) S A = (k S A) G (1 S A)$
14	1 3	nvsid	$⊢ (U \in NrmCVec \land A \in X) \to 1 S A = A$
15	9 14	mpan	$⊢ A \in X \to 1 S A = A$
16	15	adantl	$⊢ (k \in ℕ_{0} \land A \in X) \to 1 S A = A$
17	16	oveq2d	$⊢ (k \in ℕ_{0} \land A \in X) \to (k S A) G (1 S A) = (k S A) G A$
18	13 17	eqtrd	$⊢ (k \in ℕ_{0} \land A \in X) \to (k + 1) S A = (k S A) G A$
19	18	oveq1d	$⊢ (k \in ℕ_{0} \land A \in X) \to ((k + 1) S A) P B = ((k S A) G A) P B$
20	1 4	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
21	9 6 20	mp3an13	$⊢ A \in X \to A P B \in ℂ$
22	21	mulid2d	$⊢ A \in X \to 1 (A P B) = A P B$
23	22	adantl	$⊢ (k \in ℕ_{0} \land A \in X) \to 1 (A P B) = A P B$
24	23	oveq2d	$⊢ (k \in ℕ_{0} \land A \in X) \to ((k S A) P B) + 1 (A P B) = ((k S A) P B) + (A P B)$
25	1 3	nvscl	$⊢ (U \in NrmCVec \land k \in ℂ \land A \in X) \to k S A \in X$
26	9 25	mp3an1	$⊢ (k \in ℂ \land A \in X) \to k S A \in X$
27	7 26	sylan	$⊢ (k \in ℕ_{0} \land A \in X) \to k S A \in X$
28	1 2 3 4 5	ipdiri	$⊢ (k S A \in X \land A \in X \land B \in X) \to ((k S A) G A) P B = ((k S A) P B) + (A P B)$
29	6 28	mp3an3	$⊢ (k S A \in X \land A \in X) \to ((k S A) G A) P B = ((k S A) P B) + (A P B)$
30	27 29	sylancom	$⊢ (k \in ℕ_{0} \land A \in X) \to ((k S A) G A) P B = ((k S A) P B) + (A P B)$
31	24 30	eqtr4d	$⊢ (k \in ℕ_{0} \land A \in X) \to ((k S A) P B) + 1 (A P B) = ((k S A) G A) P B$
32	19 31	eqtr4d	$⊢ (k \in ℕ_{0} \land A \in X) \to ((k + 1) S A) P B = ((k S A) P B) + 1 (A P B)$
33		oveq1	$⊢ (k S A) P B = k (A P B) \to ((k S A) P B) + 1 (A P B) = k (A P B) + 1 (A P B)$
34	32 33	sylan9eq	$⊢ ((k \in ℕ_{0} \land A \in X) \land (k S A) P B = k (A P B)) \to ((k + 1) S A) P B = k (A P B) + 1 (A P B)$
35		adddir	$⊢ (k \in ℂ \land 1 \in ℂ \land A P B \in ℂ) \to (k + 1) (A P B) = k (A P B) + 1 (A P B)$
36	8 35	mp3an2	$⊢ (k \in ℂ \land A P B \in ℂ) \to (k + 1) (A P B) = k (A P B) + 1 (A P B)$
37	7 21 36	syl2an	$⊢ (k \in ℕ_{0} \land A \in X) \to (k + 1) (A P B) = k (A P B) + 1 (A P B)$
38	37	adantr	$⊢ ((k \in ℕ_{0} \land A \in X) \land (k S A) P B = k (A P B)) \to (k + 1) (A P B) = k (A P B) + 1 (A P B)$
39	34 38	eqtr4d	$⊢ ((k \in ℕ_{0} \land A \in X) \land (k S A) P B = k (A P B)) \to ((k + 1) S A) P B = (k + 1) (A P B)$
40	39	exp31	$⊢ k \in ℕ_{0} \to (A \in X \to ((k S A) P B = k (A P B) \to ((k + 1) S A) P B = (k + 1) (A P B)))$
41	40	a2d	$⊢ k \in ℕ_{0} \to ((A \in X \to (k S A) P B = k (A P B)) \to (A \in X \to ((k + 1) S A) P B = (k + 1) (A P B)))$
42		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
43	1 42 4	dip0l	$⊢ (U \in NrmCVec \land B \in X) \to 0_{vec} (U) P B = 0$
44	9 6 43	mp2an	$⊢ 0_{vec} (U) P B = 0$
45	1 3 42	nv0	$⊢ (U \in NrmCVec \land A \in X) \to 0 S A = 0_{vec} (U)$
46	9 45	mpan	$⊢ A \in X \to 0 S A = 0_{vec} (U)$
47	46	oveq1d	$⊢ A \in X \to (0 S A) P B = 0_{vec} (U) P B$
48	21	mul02d	$⊢ A \in X \to 0 \cdot (A P B) = 0$
49	44 47 48	3eqtr4a	$⊢ A \in X \to (0 S A) P B = 0 \cdot (A P B)$
50		oveq1	$⊢ j = 0 \to j S A = 0 S A$
51	50	oveq1d	$⊢ j = 0 \to (j S A) P B = (0 S A) P B$
52		oveq1	$⊢ j = 0 \to j (A P B) = 0 \cdot (A P B)$
53	51 52	eqeq12d	$⊢ j = 0 \to ((j S A) P B = j (A P B) \leftrightarrow (0 S A) P B = 0 \cdot (A P B))$
54	53	imbi2d	$⊢ j = 0 \to ((A \in X \to (j S A) P B = j (A P B)) \leftrightarrow (A \in X \to (0 S A) P B = 0 \cdot (A P B)))$
55		oveq1	$⊢ j = k \to j S A = k S A$
56	55	oveq1d	$⊢ j = k \to (j S A) P B = (k S A) P B$
57		oveq1	$⊢ j = k \to j (A P B) = k (A P B)$
58	56 57	eqeq12d	$⊢ j = k \to ((j S A) P B = j (A P B) \leftrightarrow (k S A) P B = k (A P B))$
59	58	imbi2d	$⊢ j = k \to ((A \in X \to (j S A) P B = j (A P B)) \leftrightarrow (A \in X \to (k S A) P B = k (A P B)))$
60		oveq1	$⊢ j = k + 1 \to j S A = (k + 1) S A$
61	60	oveq1d	$⊢ j = k + 1 \to (j S A) P B = ((k + 1) S A) P B$
62		oveq1	$⊢ j = k + 1 \to j (A P B) = (k + 1) (A P B)$
63	61 62	eqeq12d	$⊢ j = k + 1 \to ((j S A) P B = j (A P B) \leftrightarrow ((k + 1) S A) P B = (k + 1) (A P B))$
64	63	imbi2d	$⊢ j = k + 1 \to ((A \in X \to (j S A) P B = j (A P B)) \leftrightarrow (A \in X \to ((k + 1) S A) P B = (k + 1) (A P B)))$
65		oveq1	$⊢ j = N \to j S A = N S A$
66	65	oveq1d	$⊢ j = N \to (j S A) P B = (N S A) P B$
67		oveq1	$⊢ j = N \to j (A P B) = N (A P B)$
68	66 67	eqeq12d	$⊢ j = N \to ((j S A) P B = j (A P B) \leftrightarrow (N S A) P B = N (A P B))$
69	68	imbi2d	$⊢ j = N \to ((A \in X \to (j S A) P B = j (A P B)) \leftrightarrow (A \in X \to (N S A) P B = N (A P B)))$
70	41 49 54 59 64 69	nn0indALT	$⊢ N \in ℕ_{0} \to (A \in X \to (N S A) P B = N (A P B))$
71	70	imp	$⊢ (N \in ℕ_{0} \land A \in X) \to (N S A) P B = N (A P B)$

Metamath Proof Explorer

Theorem ipasslem1

Proof