# 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}=\mathrm{BaseSet}\left({U}\right)$
ip1i.2 ${⊢}{G}={+}_{v}\left({U}\right)$
ip1i.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
ip1i.7 ${⊢}{P}={\cdot }_{\mathrm{𝑖OLD}}\left({U}\right)$
ip1i.9 ${⊢}{U}\in {CPreHil}_{\mathrm{OLD}}$
ipasslem9.a ${⊢}{A}\in {X}$
ipasslem9.b ${⊢}{B}\in {X}$
Assertion ipasslem9 ${⊢}{C}\in ℝ\to \left({C}{S}{A}\right){P}{B}={C}\left({A}{P}{B}\right)$

### Proof

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