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

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ip1i.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
3		ip1i.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
4		ip1i.7	⊢ 𝑃 = ( ·_𝑖OLD ‘ 𝑈 )
5		ip1i.9	⊢ 𝑈 ∈ CPreHil_OLD
6		ipasslem1.b	⊢ 𝐵 ∈ 𝑋
7		nnrecre	⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℂ )
9	5	phnvi	⊢ 𝑈 ∈ NrmCVec
10	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 / 𝑁 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 )
11	9 10	mp3an1	⊢ ( ( ( 1 / 𝑁 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 )
12	8 11	sylan	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 )
13	1 4	dipcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
14	9 6 13	mp3an13	⊢ ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
15	12 14	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
16	1 4	dipcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
17	9 6 16	mp3an13	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
18		mulcl	⊢ ( ( ( 1 / 𝑁 ) ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ )
19	8 17 18	syl2an	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ )
20		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
21	20	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝑁 ∈ ℂ )
22		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
23	22	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝑁 ≠ 0 )
24	20 22	recidd	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · ( 1 / 𝑁 ) ) = 1 )
25	24	oveq1d	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 · ( 1 / 𝑁 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 1 · ( 𝐴 𝑃 𝐵 ) ) )
26	17	mulid2d	⊢ ( 𝐴 ∈ 𝑋 → ( 1 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐴 𝑃 𝐵 ) )
27	25 26	sylan9eq	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐴 𝑃 𝐵 ) )
28	24	oveq1d	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = ( 1 𝑆 𝐴 ) )
29	1 3	nvsid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
30	9 29	mpan	⊢ ( 𝐴 ∈ 𝑋 → ( 1 𝑆 𝐴 ) = 𝐴 )
31	28 30	sylan9eq	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = 𝐴 )
32	8	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 1 / 𝑁 ) ∈ ℂ )
33		simpr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
34	1 3	nvsass	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑁 ∈ ℂ ∧ ( 1 / 𝑁 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) )
35	9 34	mpan	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 1 / 𝑁 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) )
36	21 32 33 35	syl3anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) )
37	31 36	eqtr3d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝐴 = ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) )
38	37	oveq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
39		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀ )
40	39	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝑁 ∈ ℕ₀ )
41	1 2 3 4 5 6	ipasslem1	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑁 · ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
42	40 12 41	syl2anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑁 · ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
43	27 38 42	3eqtrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑁 · ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
44	17	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
45	21 32 44	mulassd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑁 · ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
46	43 45	eqtr3d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) = ( 𝑁 · ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
47	15 19 21 23 46	mulcanad	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) )

Metamath Proof Explorer

Theorem ipasslem4

Proof