Metamath Proof Explorer

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 ⊢ X = BaseSet ⁡ U
ip1i.2 ⊢ G = + v ⁡ U
ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip1i.9 ⊢ U ∈ CPreHil OLD
ipasslem9.a ⊢ A ∈ X
ipasslem9.b ⊢ B ∈ X
Assertion ipasslem9 ⊢ C ∈ ℝ → C S A P B = C ⁢ A P B

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ X = BaseSet ⁡ U
2 ip1i.2 ⊢ G = + v ⁡ U
3 ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
5 ip1i.9 ⊢ U ∈ CPreHil OLD
6 ipasslem9.a ⊢ A ∈ X
7 ipasslem9.b ⊢ B ∈ X
8 oveq1 ⊢ w = C → w S A = C S A
9 8 oveq1d ⊢ w = C → w S A P B = C S A P B
10 oveq1 ⊢ w = C → w ⁢ A P B = C ⁢ A P B
11 9 10 oveq12d ⊢ w = C → w S A P B − w ⁢ A P B = C S A P B − C ⁢ A P B
12 eqid ⊢ w ∈ ℝ ⟼ w S A P B − w ⁢ A P B = w ∈ ℝ ⟼ w S A P B − w ⁢ A P B
13 ovex ⊢ C S A P B − C ⁢ A P B ∈ V
14 11 12 13 fvmpt ⊢ C ∈ ℝ → w ∈ ℝ ⟼ w S A P B − w ⁢ A P B ⁡ C = C S A P B − C ⁢ A P B
15 1 2 3 4 5 6 7 12 ipasslem8 ⊢ w ∈ ℝ ⟼ w S A P B − w ⁢ A P B : ℝ ⟶ 0
16 fvconst ⊢ w ∈ ℝ ⟼ w S A P B − w ⁢ A P B : ℝ ⟶ 0 ∧ C ∈ ℝ → w ∈ ℝ ⟼ w S A P B − w ⁢ A P B ⁡ C = 0
17 15 16 mpan ⊢ C ∈ ℝ → w ∈ ℝ ⟼ w S A P B − w ⁢ A P B ⁡ C = 0
18 14 17 eqtr3d ⊢ C ∈ ℝ → C S A P B − C ⁢ A P B = 0
19 recn ⊢ C ∈ ℝ → C ∈ ℂ
20 5 phnvi ⊢ U ∈ NrmCVec
21 1 3 nvscl ⊢ U ∈ NrmCVec ∧ C ∈ ℂ ∧ A ∈ X → C S A ∈ X
22 20 6 21 mp3an13 ⊢ C ∈ ℂ → C S A ∈ X
23 1 4 dipcl ⊢ U ∈ NrmCVec ∧ C S A ∈ X ∧ B ∈ X → C S A P B ∈ ℂ
24 20 7 23 mp3an13 ⊢ C S A ∈ X → C S A P B ∈ ℂ
25 22 24 syl ⊢ C ∈ ℂ → C S A P B ∈ ℂ
26 1 4 dipcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ∈ ℂ
27 20 6 7 26 mp3an ⊢ A P B ∈ ℂ
28 mulcl ⊢ C ∈ ℂ ∧ A P B ∈ ℂ → C ⁢ A P B ∈ ℂ
29 27 28 mpan2 ⊢ C ∈ ℂ → C ⁢ A P B ∈ ℂ
30 25 29 subeq0ad ⊢ C ∈ ℂ → C S A P B − C ⁢ A P B = 0 ↔ C S A P B = C ⁢ A P B
31 19 30 syl ⊢ C ∈ ℝ → C S A P B − C ⁢ A P B = 0 ↔ C S A P B = C ⁢ A P B
32 18 31 mpbid ⊢ C ∈ ℝ → C S A P B = C ⁢ A P B