Theorem ipasslem9

Description: Lemma for ipassi . Conclude from ipasslem8 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip1i.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ip1i.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	ip1i.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	ip1i.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
	ip1i.9	⊢ 𝑈 ∈ CPreHilOLD
	ipasslem9.a	⊢ 𝐴 ∈ 𝑋
	ipasslem9.b	⊢ 𝐵 ∈ 𝑋
Assertion	ipasslem9	⊢ ( 𝐶 ∈ ℝ → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )

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		ipasslem9.a	⊢ 𝐴 ∈ 𝑋
7		ipasslem9.b	⊢ 𝐵 ∈ 𝑋
8		oveq1	⊢ ( 𝑤 = 𝐶 → ( 𝑤 𝑆 𝐴 ) = ( 𝐶 𝑆 𝐴 ) )
9	8	oveq1d	⊢ ( 𝑤 = 𝐶 → ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) )
10		oveq1	⊢ ( 𝑤 = 𝐶 → ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )
11	9 10	oveq12d	⊢ ( 𝑤 = 𝐶 → ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) = ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
12		eqid	⊢ ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) = ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) )
13		ovex	⊢ ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) ∈ V
14	11 12 13	fvmpt	⊢ ( 𝐶 ∈ ℝ → ( ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) ‘ 𝐶 ) = ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
15	1 2 3 4 5 6 7 12	ipasslem8	⊢ ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) : ℝ ⟶ { 0 }
16		fvconst	⊢ ( ( ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) : ℝ ⟶ { 0 } ∧ 𝐶 ∈ ℝ ) → ( ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) ‘ 𝐶 ) = 0 )
17	15 16	mpan	⊢ ( 𝐶 ∈ ℝ → ( ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) ‘ 𝐶 ) = 0 )
18	14 17	eqtr3d	⊢ ( 𝐶 ∈ ℝ → ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) = 0 )
19		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
20	5	phnvi	⊢ 𝑈 ∈ NrmCVec
21	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝐶 𝑆 𝐴 ) ∈ 𝑋 )
22	20 6 21	mp3an13	⊢ ( 𝐶 ∈ ℂ → ( 𝐶 𝑆 𝐴 ) ∈ 𝑋 )
23	1 4	dipcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐶 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
24	20 7 23	mp3an13	⊢ ( ( 𝐶 𝑆 𝐴 ) ∈ 𝑋 → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
25	22 24	syl	⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
26	1 4	dipcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
27	20 6 7 26	mp3an	⊢ ( 𝐴 𝑃 𝐵 ) ∈ ℂ
28		mulcl	⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ )
29	27 28	mpan2	⊢ ( 𝐶 ∈ ℂ → ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ )
30	25 29	subeq0ad	⊢ ( 𝐶 ∈ ℂ → ( ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) = 0 ↔ ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
31	19 30	syl	⊢ ( 𝐶 ∈ ℝ → ( ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) = 0 ↔ ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
32	18 31	mpbid	⊢ ( 𝐶 ∈ ℝ → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )