Theorem 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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ip1i.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	ip1i.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	ip1i.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
	ip1i.9	⊢ 𝑈 ∈ CPreHilOLD
	ipasslem1.b	⊢ 𝐵 ∈ 𝑋
Assertion	ipasslem1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )

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		nn0cn	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
8		ax-1cn	⊢ 1 ∈ ℂ
9	5	phnvi	⊢ 𝑈 ∈ NrmCVec
10	1 2 3	nvdir	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
11	9 10	mpan	⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
12	8 11	mp3an2	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
13	7 12	sylan	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
14	1 3	nvsid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
15	9 14	mpan	⊢ ( 𝐴 ∈ 𝑋 → ( 1 𝑆 𝐴 ) = 𝐴 )
16	15	adantl	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
17	16	oveq2d	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) )
18	13 17	eqtrd	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) 𝑆 𝐴 ) = ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) )
19	18	oveq1d	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) )
20	1 4	dipcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
21	9 6 20	mp3an13	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
22	21	mullidd	⊢ ( 𝐴 ∈ 𝑋 → ( 1 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐴 𝑃 𝐵 ) )
23	22	adantl	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( 1 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐴 𝑃 𝐵 ) )
24	23	oveq2d	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 𝐴 𝑃 𝐵 ) ) )
25	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 )
26	9 25	mp3an1	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 )
27	7 26	sylan	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 )
28	1 2 3 4 5	ipdiri	⊢ ( ( ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 𝐴 𝑃 𝐵 ) ) )
29	6 28	mp3an3	⊢ ( ( ( 𝑘 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 𝐴 𝑃 𝐵 ) ) )
30	27 29	sylancom	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 𝐴 𝑃 𝐵 ) ) )
31	24 30	eqtr4d	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝐺 𝐴 ) 𝑃 𝐵 ) )
32	19 31	eqtr4d	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
33		oveq1	⊢ ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) → ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
34	32 33	sylan9eq	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
35		adddir	⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
36	8 35	mp3an2	⊢ ( ( 𝑘 ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
37	7 21 36	syl2an	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
38	37	adantr	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) + ( 1 · ( 𝐴 𝑃 𝐵 ) ) ) )
39	34 38	eqtr4d	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) )
40	39	exp31	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐴 ∈ 𝑋 → ( ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) ) ) )
41	40	a2d	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) → ( 𝐴 ∈ 𝑋 → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) ) ) )
42		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
43	1 42 4	dip0l	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) = 0 )
44	9 6 43	mp2an	⊢ ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) = 0
45	1 3 42	nv0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 0 𝑆 𝐴 ) = ( 0vec ‘ 𝑈 ) )
46	9 45	mpan	⊢ ( 𝐴 ∈ 𝑋 → ( 0 𝑆 𝐴 ) = ( 0vec ‘ 𝑈 ) )
47	46	oveq1d	⊢ ( 𝐴 ∈ 𝑋 → ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) )
48	21	mul02d	⊢ ( 𝐴 ∈ 𝑋 → ( 0 · ( 𝐴 𝑃 𝐵 ) ) = 0 )
49	44 47 48	3eqtr4a	⊢ ( 𝐴 ∈ 𝑋 → ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 0 · ( 𝐴 𝑃 𝐵 ) ) )
50		oveq1	⊢ ( 𝑗 = 0 → ( 𝑗 𝑆 𝐴 ) = ( 0 𝑆 𝐴 ) )
51	50	oveq1d	⊢ ( 𝑗 = 0 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) )
52		oveq1	⊢ ( 𝑗 = 0 → ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) = ( 0 · ( 𝐴 𝑃 𝐵 ) ) )
53	51 52	eqeq12d	⊢ ( 𝑗 = 0 → ( ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 0 · ( 𝐴 𝑃 𝐵 ) ) ) )
54	53	imbi2d	⊢ ( 𝑗 = 0 → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( ( 0 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 0 · ( 𝐴 𝑃 𝐵 ) ) ) ) )
55		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 𝑆 𝐴 ) = ( 𝑘 𝑆 𝐴 ) )
56	55	oveq1d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) )
57		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) )
58	56 57	eqeq12d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) )
59	58	imbi2d	⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( ( 𝑘 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑘 · ( 𝐴 𝑃 𝐵 ) ) ) ) )
60		oveq1	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 𝑆 𝐴 ) = ( ( 𝑘 + 1 ) 𝑆 𝐴 ) )
61	60	oveq1d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) )
62		oveq1	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) )
63	61 62	eqeq12d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
64	63	imbi2d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( ( ( 𝑘 + 1 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑘 + 1 ) · ( 𝐴 𝑃 𝐵 ) ) ) ) )
65		oveq1	⊢ ( 𝑗 = 𝑁 → ( 𝑗 𝑆 𝐴 ) = ( 𝑁 𝑆 𝐴 ) )
66	65	oveq1d	⊢ ( 𝑗 = 𝑁 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) )
67		oveq1	⊢ ( 𝑗 = 𝑁 → ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )
68	66 67	eqeq12d	⊢ ( 𝑗 = 𝑁 → ( ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) ) )
69	68	imbi2d	⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑗 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) ) ) )
70	41 49 54 59 64 69	nn0indALT	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ 𝑋 → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) ) )
71	70	imp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑁 · ( 𝐴 𝑃 𝐵 ) ) )