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∈CPreHilOLD
ipasslem9.a ⊢A∈X
ipasslem9.b ⊢B∈X
Assertion ipasslem9 ⊢C∈ℝ→CSAPB=C⁢APB

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∈CPreHilOLD
6 ipasslem9.a ⊢A∈X
7 ipasslem9.b ⊢B∈X
8 oveq1 ⊢w=C→wSA=CSA
9 8 oveq1d ⊢w=C→wSAPB=CSAPB
10 oveq1 ⊢w=C→w⁢APB=C⁢APB
11 9 10 oveq12d ⊢w=C→wSAPB−w⁢APB=CSAPB−C⁢APB
12 eqid ⊢w∈ℝ⟼wSAPB−w⁢APB=w∈ℝ⟼wSAPB−w⁢APB
13 ovex ⊢CSAPB−C⁢APB∈V
14 11 12 13 fvmpt ⊢C∈ℝ→w∈ℝ⟼wSAPB−w⁢APB⁡C=CSAPB−C⁢APB
15 1 2 3 4 5 6 7 12 ipasslem8 ⊢w∈ℝ⟼wSAPB−w⁢APB:ℝ⟶0
16 fvconst ⊢w∈ℝ⟼wSAPB−w⁢APB:ℝ⟶0∧C∈ℝ→w∈ℝ⟼wSAPB−w⁢APB⁡C=0
17 15 16 mpan ⊢C∈ℝ→w∈ℝ⟼wSAPB−w⁢APB⁡C=0
18 14 17 eqtr3d ⊢C∈ℝ→CSAPB−C⁢APB=0
19 recn ⊢C∈ℝ→C∈ℂ
20 5 phnvi ⊢U∈NrmCVec
21 1 3 nvscl ⊢U∈NrmCVec∧C∈ℂ∧A∈X→CSA∈X
22 20 6 21 mp3an13 ⊢C∈ℂ→CSA∈X
23 1 4 dipcl ⊢U∈NrmCVec∧CSA∈X∧B∈X→CSAPB∈ℂ
24 20 7 23 mp3an13 ⊢CSA∈X→CSAPB∈ℂ
25 22 24 syl ⊢C∈ℂ→CSAPB∈ℂ
26 1 4 dipcl ⊢U∈NrmCVec∧A∈X∧B∈X→APB∈ℂ
27 20 6 7 26 mp3an ⊢APB∈ℂ
28 mulcl ⊢C∈ℂ∧APB∈ℂ→C⁢APB∈ℂ
29 27 28 mpan2 ⊢C∈ℂ→C⁢APB∈ℂ
30 25 29 subeq0ad ⊢C∈ℂ→CSAPB−C⁢APB=0↔CSAPB=C⁢APB
31 19 30 syl ⊢C∈ℝ→CSAPB−C⁢APB=0↔CSAPB=C⁢APB
32 18 31 mpbid ⊢C∈ℝ→CSAPB=C⁢APB